defpred S₁[ set ] means ex B being Element of FX st
( B in FX & $1 = B \ (PartUnion (B,R)) );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool (union FX) & S₁[x] ) ) from XFAMILY:sch 1();
reconsider X = X as set ;
take X ; :: thesis: for A being set holds
( A in X iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) )
let A be set ; :: thesis: ( A in X iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) )
thus ( A in X implies ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) by A1; :: thesis: ( ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) implies A in X )
assume A2: ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ; :: thesis: A in X
then A c= union FX by XBOOLE_1:109, ZFMISC_1:74;
hence A in X by A1, A2; :: thesis: verum