n:{1...}, E:(
n
nProp).
(EquivRel i,j:n. i E j) 
(x:i,j:n//(i E j). 
x = n-1 
i,j:n//(i E j) x i,j:(n-1)//(i E j))
incl_aux4_quo
A == A False
Thm* n:{1...}, E:(nnProp).
(EquivRel i,j:n. i E j)
(x:i,j:n//(i E j). x = n-1 i,j:n//(i E j) x i,j:(n-1)//(i E j))
incl_aux4_quo