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