let X, Y be set ; :: thesis: (proj2_4 X) \ (proj2_4 Y) c= proj2_4 (X \ Y)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (proj2_4 X) \ (proj2_4 Y) or x in proj2_4 (X \ Y) )
assume A1: x in (proj2_4 X) \ (proj2_4 Y) ; :: thesis: x in proj2_4 (X \ Y)
then x in proj2_4 X by XBOOLE_0:def 5;
then consider x1, x2, x3 being set such that
A2: [x1,x,x2,x3] in X by Th20;
not x in proj2_4 Y by A1, XBOOLE_0:def 5;
then not [x1,x,x2,x3] in Y by Th20a;
then [x1,x,x2,x3] in X \ Y by A2, XBOOLE_0:def 5;
hence x in proj2_4 (X \ Y) by Th20a; :: thesis: verum