let I be set ; :: thesis: for X, Y being ManySortedSet of I holds
( X c= X \/ Y & Y c= X \/ Y )
let X, Y be ManySortedSet of I; :: thesis: ( X c= X \/ Y & Y c= X \/ Y )
thus X c= X \/ Y :: thesis: Y c= X \/ Y

proof

let i be set ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies X . i c= (X \/ Y) . i )
assume A1: i in I ; :: thesis: X . i c= (X \/ Y) . i
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in X . i or e in (X \/ Y) . i )
assume e in X . i ; :: thesis: e in (X \/ Y) . i
then e in (X . i) \/ (Y . i) by XBOOLE_0:def 3;
hence e in (X \/ Y) . i by A1, Def7; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 2 :: thesis: ( i in I implies Y . i c= (X \/ Y) . i )
assume A2: i in I ; :: thesis: Y . i c= (X \/ Y) . i
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in Y . i or e in (X \/ Y) . i )
assume e in Y . i ; :: thesis: e in (X \/ Y) . i
then e in (X . i) \/ (Y . i) by XBOOLE_0:def 3;
hence e in (X \/ Y) . i by A2, Def7; :: thesis: verum