let S be non empty non void ManySortedSign ; :: thesis: for A being MSAlgebra over 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 over 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:12;
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;
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 object ; :: 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:19;
then [q,y] in C1 . i by A2, A3, A5, RELAT_2:def 8;
hence q in Class (C2,y) by A4, EQREL_1:19; :: thesis: verum

end;

assume A is non-empty ; :: thesis: Class (C1,y) c= Class (C2,x)
then reconsider B = A as non-empty MSAlgebra over S ;
field (C1 . i) = the Sorts of A . i by ORDERS_1:12;
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 object ; :: 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:19;
then [q,x] in C1 . i by A3, A7, A6, RELAT_2:def 8;
hence q in Class (C2,x) by A4, EQREL_1:19; :: thesis: verum