let I be set ; :: thesis: for x, A, B being ManySortedSet of I holds
( A (\/) {x} c= B iff ( x in B & A c= B ) )
let x, A, B be ManySortedSet of I; :: 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 :: thesis: for i being object st i in I holds
(A . i) \/ {(x . i)} c= B . i
let i be object ; :: 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;
then (A . i) \/ ({x} . i) c= B . i by A3, PBOOLE:def 4;
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 object ; :: according to PBOOLE:def 1 :: 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 ZFMISC_1:137; :: thesis: verum
end;
let i be object ; :: according to PBOOLE:def 2 :: 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 ZFMISC_1:137; :: thesis: verum
end;
assume that
A4: x in B and
A5: A c= B ; :: thesis: A (\/) {x} c= B
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or (A (\/) {x}) . i c= B . i )
assume A6: i in I ; :: thesis: (A (\/) {x}) . i c= B . i
then A7: x . i in B . i by A4;
A . i c= B . i by A5, A6;
then (A . i) \/ {(x . i)} c= B . i by A7, ZFMISC_1:137;
then (A . i) \/ ({x} . i) c= B . i by A6, Def1;
hence (A (\/) {x}) . i c= B . i by A6, PBOOLE:def 4; :: thesis: verum