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 XBOOLE_0: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 consider B being Element of FX such that
A3: ( B in FX & A = B \ (PartUnion B,R) ) ;
A c= union FX by A3, XBOOLE_1:109, ZFMISC_1:92;
hence A in X by A1, A2; :: thesis: verum