let I be set ; :: thesis: for x, y, X being ManySortedSet of I holds
( {x,y} \ X = [[0]] I iff ( x in X & y in X ) )
let x, y, X be ManySortedSet of I; :: thesis: ( {x,y} \ X = [[0]] I iff ( x in X & y in X ) )
thus ( {x,y} \ X = [[0]] I implies ( x in X & y in X ) ) :: thesis: ( x in X & y in X implies {x,y} \ X = [[0]] I )

proof

assume A1: {x,y} \ X = [[0]] I ; :: thesis: ( x in X & y in X )
thus x in X :: thesis: y in X

proof

let i be set ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or x . i in X . i )
assume A2: i in I ; :: thesis: x . i in X . i
then {(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by Def2
.= ({x,y} \ X) . i by A2, PBOOLE:def 6
.= {} by A1, PBOOLE:5 ;
hence x . i in X . i by ZFMISC_1:64; :: thesis: verum

end;

let i be set ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or y . i in X . i )
assume A3: i in I ; :: thesis: y . i in X . i
then {(x . i),(y . i)} \ (X . i) = ({x,y} . i) \ (X . i) by Def2
.= ({x,y} \ X) . i by A3, PBOOLE:def 6
.= {} by A1, PBOOLE:5 ;
hence y . i in X . i by ZFMISC_1:64; :: thesis: verum

end;

assume that
A4: x in X and
A5: y in X ; :: thesis: {x,y} \ X = [[0]] I

now

let i be set ; :: thesis: ( i in I implies ({x,y} \ X) . i = ([[0]] I) . i )
assume A6: i in I ; :: thesis: ({x,y} \ X) . i = ([[0]] I) . i
then A7: x . i in X . i by A4, PBOOLE:def 1;
A8: y . i in X . i by A5, A6, PBOOLE:def 1;
thus ({x,y} \ X) . i = ({x,y} . i) \ (X . i) by A6, PBOOLE:def 6
.= {(x . i),(y . i)} \ (X . i) by A6, Def2
.= {} by A7, A8, ZFMISC_1:64
.= ([[0]] I) . i by PBOOLE:5 ; :: thesis: verum

end;

hence {x,y} \ X = [[0]] I by PBOOLE:3; :: thesis: verum