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