let I be set ; :: thesis: for A, x, B being ManySortedSet of holds
( A \/ {x} c= B iff ( x in B & A c= B ) )
let A, x, B be ManySortedSet of ; :: thesis: ( A \/ {x} c= B iff ( x in B & A c= B ) )
thus ( A \/ {x} c= B implies ( x in B & A c= B ) ) :: thesis: ( x in B & A c= B implies A \/ {x} c= B )

proof

assume A1: A \/ {x} c= B ; :: thesis: ( x in B & A c= B )

A2: now

let i be set ; :: thesis: ( i in I implies (A . i) \/ {(x . i)} c= B . i )
assume A3: i in I ; :: thesis: (A . i) \/ {(x . i)} c= B . i
then (A \/ {x}) . i c= B . i by A1, PBOOLE:def 5;
then (A . i) \/ ({x} . i) c= B . i by A3, PBOOLE:def 7;
hence (A . i) \/ {(x . i)} c= B . i by A3, Def1; :: thesis: verum

end;

thus x in B :: thesis: A c= B

proof

let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or x . i in B . i )
assume i in I ; :: thesis: x . i in B . i
then (A . i) \/ {(x . i)} c= B . i by A2;
hence x . i in B . i by SETWISEO:8; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or A . i c= B . i )
assume i in I ; :: thesis: A . i c= B . i
then (A . i) \/ {(x . i)} c= B . i by A2;
hence A . i c= B . i by SETWISEO:8; :: thesis: verum

end;

assume A4: ( x in B & A c= B ) ; :: thesis: A \/ {x} c= B
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or (A \/ {x}) . i c= B . i )
assume A5: i in I ; :: thesis: (A \/ {x}) . i c= B . i
then ( x . i in B . i & A . i c= B . i ) by A4, PBOOLE:def 4, PBOOLE:def 5;
then (A . i) \/ {(x . i)} c= B . i by SETWISEO:8;
then (A . i) \/ ({x} . i) c= B . i by A5, Def1;
hence (A \/ {x}) . i c= B . i by A5, PBOOLE:def 7; :: thesis: verum