let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra of S
for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) )
let A be MSAlgebra of S; :: thesis: for C1, C2 being MSEquivalence-like ManySortedRelation of A st C1 c= C2 holds
for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) )
let C1, C2 be MSEquivalence-like ManySortedRelation of A; :: thesis: ( C1 c= C2 implies for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) ) )
assume A1: C1 c= C2 ; :: thesis: for i being Element of S
for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) )
let i be Element of S; :: thesis: for x, y being Element of the Sorts of A . i st [x,y] in C1 . i holds
( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) )
let x, y be Element of the Sorts of A . i; :: thesis: ( [x,y] in C1 . i implies ( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) ) )
assume A2: [x,y] in C1 . i ; :: thesis: ( Class C1,x c= Class C2,y & ( A is non-empty implies Class C1,y c= Class C2,x ) )
field (C1 . i) = the Sorts of A . i by ORDERS_1:97;
then A3: C1 . i is_transitive_in the Sorts of A . i by RELAT_2:def 16;
A4: C1 . i c= C2 . i by A1, PBOOLE:def 5;
thus Class C1,x c= Class C2,y :: thesis: ( A is non-empty implies Class C1,y c= Class C2,x )

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Class C1,x or q in Class C2,y )
assume A5: q in Class C1,x ; :: thesis: q in Class C2,y
then [q,x] in C1 . i by EQREL_1:27;
then [q,y] in C1 . i by A2, A3, A5, RELAT_2:def 8;
hence q in Class C2,y by A4, EQREL_1:27; :: thesis: verum

end;

assume A is non-empty ; :: thesis: Class C1,y c= Class C2,x
then reconsider B = A as non-empty MSAlgebra of S ;
field (C1 . i) = the Sorts of A . i by ORDERS_1:97;
then C1 . i is_symmetric_in the Sorts of B . i by RELAT_2:def 11;
then A6: [y,x] in C1 . i by A2, RELAT_2:def 3;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in Class C1,y or q in Class C2,x )
assume A7: q in Class C1,y ; :: thesis: q in Class C2,x
[q,y] in C1 . i by A7, EQREL_1:27;
then [q,x] in C1 . i by A3, A7, A6, RELAT_2:def 8;
hence q in Class C2,x by A4, EQREL_1:27; :: thesis: verum