1
1Prop2. EquivRel x,y:
1. x E y3.
x,y:1. Dec(x E y)
m:(1+1). m ~ (i,j:1//(i E j)) E:(11Prop).
(EquivRel x,y:1. x E y) & (x,y:1. Dec(x E y)) 
(m:(1+1). m ~ (i,j:1//(i E j)))| 1 | 1. E: 11Prop 2. EquivRel x,y: 1. x E y3. x,y:1. Dec(x E y) m:(1+1). m ~ (i,j:1//(i E j)) |
About:
 |  |  |  |  |
 |  |  |  |