2. m:
n3. E:
n
nProp4. EquivRel x,y:
n. x E y5. z: x,y:
m//(x E y)
z 
x,y:n//(x E y)2. m:
n3. E:
nnProp4. EquivRel x,y:
n. x E y EquivRel x,y:m. x E y 
n:{1...}, m:n, E:(nnProp).
(EquivRel x,y:n. x E y) 
(z:x,y:m//(x E y). z x,y:n//(x E y))| 1 | 1. n: {1...} 2. m: n3. E: nnProp4. EquivRel x,y: n. x E y5. z: x,y: m//(x E y) z x,y:n//(x E y) |
| 2 | 1. n: {1...} 2. m: n3. E: nnProp4. EquivRel x,y: n. x E y EquivRel x,y:m. x E y |
About:
 |  |  |  |  |  |  |