let X, Y be set ; (proj1_4 X) \ (proj1_4 Y) c= proj1_4 (X \ Y)
let x be object ; TARSKI:def 3 ( not x in (proj1_4 X) \ (proj1_4 Y) or x in proj1_4 (X \ Y) )
assume A1:
x in (proj1_4 X) \ (proj1_4 Y)
; x in proj1_4 (X \ Y)
then
x in proj1_4 X
by XBOOLE_0:def 5;
then consider x1, x2, x3 being object such that
A2:
[x,x1,x2,x3] in X
by Th18;
not x in proj1_4 Y
by A1, XBOOLE_0:def 5;
then
not [x,x1,x2,x3] in Y
by Th19;
then
[x,x1,x2,x3] in X \ Y
by A2, XBOOLE_0:def 5;
hence
x in proj1_4 (X \ Y)
by Th19; verum