let I be set ; :: thesis: for x1, x2, X being ManySortedSet of holds
( {x1,x2} c= X iff ( x1 in X & x2 in X ) )
let x1, x2, X be ManySortedSet of ; :: 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 A4: ( x1 in X & 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 A5: i in I ; :: thesis: {x1,x2} . i c= X . i
then ( x1 . i in X . i & x2 . i in X . i ) by A4, PBOOLE:def 4;
then {(x1 . i),(x2 . i)} c= X . i by ZFMISC_1:38;
hence {x1,x2} . i c= X . i by A5, Def2; :: thesis: verum