let I be set ; :: thesis: for x1, x2, X being ManySortedSet of I holds
( {x1,x2} c= X iff ( x1 in X & x2 in X ) )
let x1, x2, X be ManySortedSet of I; :: thesis: ( {x1,x2} c= X iff ( x1 in X & x2 in X ) )
thus ( {x1,x2} c= X implies ( x1 in X & x2 in X ) ) :: thesis: ( x1 in X & x2 in X implies {x1,x2} c= X )
proof
assume A1: {x1,x2} c= X ; :: thesis: ( x1 in X & x2 in X )
thus x1 in X :: thesis: x2 in X
proof
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x1 . i in X . i )
assume A2: i in I ; :: thesis: x1 . i in X . i
then {x1,x2} . i c= X . i by A1;
then {(x1 . i),(x2 . i)} c= X . i by A2, Def2;
hence x1 . i in X . i by ZFMISC_1:32; :: thesis: verum
end;
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x2 . i in X . i )
assume A3: i in I ; :: thesis: x2 . i in X . i
then {x1,x2} . i c= X . i by A1;
then {(x1 . i),(x2 . i)} c= X . i by A3, Def2;
hence x2 . i in X . i by ZFMISC_1:32; :: thesis: verum
end;
assume that
A4: x1 in X and
A5: x2 in X ; :: thesis: {x1,x2} c= X
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or {x1,x2} . i c= X . i )
assume A6: i in I ; :: thesis: {x1,x2} . i c= X . i
then A7: x1 . i in X . i by A4;
x2 . i in X . i by A5, A6;
then {(x1 . i),(x2 . i)} c= X . i by A7, ZFMISC_1:32;
hence {x1,x2} . i c= X . i by A6, Def2; :: thesis: verum