Thm* n:{1...}, m:n, E:(nnProp). Sym x,y:n. x E y Sym x,y:m. x E y rest_symm_rel
In prior sections: rel 1
n:{1...}, m:
n, E:(n
nProp). Sym x,y:n. x E y 
Sym x,y:m. x E y
rest_symm_rel
a,b:T. E(a;b) E(b;a)
n:{1...}, m:n, E:(nnProp). Sym x,y:n. x E y Sym x,y:m. x E y
rest_symm_rel