let X, Y be set ; :: thesis: (proj2 X) \ (proj2 Y) c= proj2 (X \ Y)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (proj2 X) \ (proj2 Y) or y in proj2 (X \ Y) )
assume A1: y in (proj2 X) \ (proj2 Y) ; :: thesis: y in proj2 (X \ Y)
then y in proj2 X by XBOOLE_0:def 5;
then consider x being object such that
A2: [x,y] in X by Def13;
not y in proj2 Y by A1, XBOOLE_0:def 5;
then not [x,y] in Y by Def13;
then [x,y] in X \ Y by A2, XBOOLE_0:def 5;
hence y in proj2 (X \ Y) by Def13; :: thesis: verum