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