At: rest equi rel 1 1 2 1
1. n: {1...}
2. m:
n
3. E:
n

n
Prop
4. Refl(
n;x,y.x E y)
5. Sym x,y:
n. x E y
6. Trans x,y:
n. x E y
Sym x,y:
m. x E y
By: BackThru
Thm*
n:{1...}, m:
n, E:(
n

n
Prop). Sym x,y:
n. x E y 
Sym x,y:
m. x E y
Generated subgoals:None
About: