let X, Y, Z be set ; :: thesis: ( X c= Y implies X misses Z \ Y )
assume A1: X c= Y ; :: thesis: X misses Z \ Y
thus X /\ (Z \ Y) = (Z /\ X) \ Y by Th49
.= Z /\ (X \ Y) by Th49
.= Z /\ {} by A1, Lm1
.= {} ; :: according to XBOOLE_0:def 7 :: thesis: verum