let I be non empty set ; :: thesis: for M being ManySortedSet of I

for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (\/) EqR2 c= EqR1 "\/" EqR2

let M be ManySortedSet of I; :: thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (\/) EqR2 c= EqR1 "\/" EqR2

let EqR1, EqR2 be Equivalence_Relation of M; :: thesis: EqR1 (\/) EqR2 c= EqR1 "\/" EqR2

consider EqR3 being ManySortedRelation of M such that

A1: EqR3 = EqR1 (\/) EqR2 and

A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4;

for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (\/) EqR2 c= EqR1 "\/" EqR2

let M be ManySortedSet of I; :: thesis: for EqR1, EqR2 being Equivalence_Relation of M holds EqR1 (\/) EqR2 c= EqR1 "\/" EqR2

let EqR1, EqR2 be Equivalence_Relation of M; :: thesis: EqR1 (\/) EqR2 c= EqR1 "\/" EqR2

consider EqR3 being ManySortedRelation of M such that

A1: EqR3 = EqR1 (\/) EqR2 and

A2: EqR1 "\/" EqR2 = EqCl EqR3 by Def4;

now :: thesis: for i being object st i in I holds

EqR3 . i c= (EqR1 "\/" EqR2) . i

hence
EqR1 (\/) EqR2 c= EqR1 "\/" EqR2
by A1, PBOOLE:def 2; :: thesis: verumEqR3 . i c= (EqR1 "\/" EqR2) . i

let i be object ; :: thesis: ( i in I implies EqR3 . i c= (EqR1 "\/" EqR2) . i )

assume i in I ; :: thesis: EqR3 . i c= (EqR1 "\/" EqR2) . i

then reconsider i9 = i as Element of I ;

EqR3 . i c= EqCl (EqR3 . i9) by Def1;

hence EqR3 . i c= (EqR1 "\/" EqR2) . i by A2, Def3; :: thesis: verum

end;assume i in I ; :: thesis: EqR3 . i c= (EqR1 "\/" EqR2) . i

then reconsider i9 = i as Element of I ;

EqR3 . i c= EqCl (EqR3 . i9) by Def1;

hence EqR3 . i c= (EqR1 "\/" EqR2) . i by A2, Def3; :: thesis: verum