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 set ; :: according to PBOOLE:def 4 :: 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, PBOOLE:def 5;
then {(x1 . i),(x2 . i)} c= X . i by A2, Def2;
hence x1 . i in X . i by ZFMISC_1:38; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 4 :: 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, PBOOLE:def 5;
then {(x1 . i),(x2 . i)} c= X . i by A3, Def2;
hence x2 . i in X . i by ZFMISC_1:38; :: thesis: verum

end;

assume that
A4: x1 in X and
A5: x2 in X ; :: thesis: {x1,x2} c= X
let i be set ; :: according to PBOOLE:def 5 :: 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, PBOOLE:def 4;
x2 . i in X . i by A5, A6, PBOOLE:def 4;
then {(x1 . i),(x2 . i)} c= X . i by A7, ZFMISC_1:38;
hence {x1,x2} . i c= X . i by A6, Def2; :: thesis: verum