let X, Y be set ; :: thesis: ( (proj1 X) \ (proj1 Y) c= proj1 (X \ Y) & (proj2 X) \ (proj2 Y) c= proj2 (X \ Y) )
thus (proj1 X) \ (proj1 Y) c= proj1 (X \ Y) :: thesis: (proj2 X) \ (proj2 Y) c= proj2 (X \ Y)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj1 X) \ (proj1 Y) or x in proj1 (X \ Y) )
assume A1: x in (proj1 X) \ (proj1 Y) ; :: thesis: x in proj1 (X \ Y)
then A2: ( x in proj1 X & not x in proj1 Y ) by XBOOLE_0:def 5;
consider y being set such that
A3: [x,y] in X by A1, RELAT_1:def 4;
not [x,y] in Y by A2, RELAT_1:def 4;
then [x,y] in X \ Y by A3, XBOOLE_0:def 5;
hence x in proj1 (X \ Y) by RELAT_1:def 4; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (proj2 X) \ (proj2 Y) or y in proj2 (X \ Y) )
assume A4: y in (proj2 X) \ (proj2 Y) ; :: thesis: y in proj2 (X \ Y)
then A5: ( y in proj2 X & not y in proj2 Y ) by XBOOLE_0:def 5;
consider x being set such that
A6: [x,y] in X by A4, RELAT_1:def 5;
not [x,y] in Y by A5, RELAT_1:def 5;
then [x,y] in X \ Y by A6, XBOOLE_0:def 5;
hence y in proj2 (X \ Y) by RELAT_1:def 5; :: thesis: verum