let X, Y, Z be set ; :: thesis: ( X c= Y \/ Z & X misses Z implies X c= Y )
assume that
A1: X c= Y \/ Z and
A2: X /\ Z = {} ; :: according to XBOOLE_0:def 7 :: thesis: X c= Y
X /\ (Y \/ Z) = X by A1, Th28;
then (Y /\ X) \/ {} = X by A2, Th23;
hence X c= Y by Th17; :: thesis: verum