At: incl aux3 quo 1 2 1 2 2 1 2 2
1. n: {1...}
2. m: 
n
3. E: n
nProp
4. EquivRel i,j:n. i E j
5. EquivRel i,j:m. i E j
6. x: i,j:m//(i E j)
7. y: i,j:m//(i E j)
8. x 
i,j:n//(i E j)
9. y i,j:n//(i E j)
10. y1: m
11. y2: m
12. y1 E y2
13. x1: m
14. x2: m
15. x1 E x2
x1 i,j:n//(i E j)
By:
Assert (x1 n)
THEN
Inclusion 16
Generated subgoals:None
About:
