let A, B, X be set ; :: thesis: ( X c= union (A \/ B) & ( for Y being set st Y in B holds

Y misses X ) implies X c= union A )

assume X c= union (A \/ B) ; :: thesis: ( ex Y being set st

( Y in B & not Y misses X ) or X c= union A )

then X c= (union (A \/ B)) /\ X by XBOOLE_1:19;

then X c= ((union A) \/ (union B)) /\ X by ZFMISC_1:78;

then A1: X c= ((union A) /\ X) \/ ((union B) /\ X) by XBOOLE_1:23;

assume for Y being set st Y in B holds

Y misses X ; :: thesis: X c= union A

then union B misses X by ZFMISC_1:80;

then A2: (union B) /\ X = {} ;

(union A) /\ X c= union A by XBOOLE_1:17;

hence X c= union A by A2, A1; :: thesis: verum

Y misses X ) implies X c= union A )

assume X c= union (A \/ B) ; :: thesis: ( ex Y being set st

( Y in B & not Y misses X ) or X c= union A )

then X c= (union (A \/ B)) /\ X by XBOOLE_1:19;

then X c= ((union A) \/ (union B)) /\ X by ZFMISC_1:78;

then A1: X c= ((union A) /\ X) \/ ((union B) /\ X) by XBOOLE_1:23;

assume for Y being set st Y in B holds

Y misses X ; :: thesis: X c= union A

then union B misses X by ZFMISC_1:80;

then A2: (union B) /\ X = {} ;

(union A) /\ X c= union A by XBOOLE_1:17;

hence X c= union A by A2, A1; :: thesis: verum