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 A1: X c= union (A \/ B) ; :: thesis: ( ex Y being set st
( Y in B & not Y misses X ) or X c= union A )
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:98;
then A2: (union B) /\ X = {} by XBOOLE_0:def 7;
X c= (union (A \/ B)) /\ X by A1, XBOOLE_1:19;
then X c= ((union A) \/ (union B)) /\ X by ZFMISC_1:96;
then A3: X c= ((union A) /\ X) \/ ((union B) /\ X) by XBOOLE_1:23;
(union A) /\ X c= union A by XBOOLE_1:17;
hence X c= union A by A2, A3, XBOOLE_1:1; :: thesis: verum