defpred S₁[ set ] means ex x being object st
( x in X & $1 = {x} );
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff S₁[A] ) from SUBSET_1:sch 3();
A2: for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) )

proof

let A be Subset of X; :: thesis: ( A in F implies ( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) )
assume A in F ; :: thesis: ( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) )
then consider x being object such that
x in X and
A3: A = {x} by A1;
thus A <> {} by A3; :: thesis: for B being Subset of X holds
( not B in F or A = B or A misses B )
let B be Subset of X; :: thesis: ( not B in F or A = B or A misses B )
assume B in F ; :: thesis: ( A = B or A misses B )
then consider y being object such that
y in X and
A4: B = {y} by A1;

now :: thesis: ( not x = y implies A misses B )

assume A5: not x = y ; :: thesis: A misses B
for z being object st z in A holds
not z in B

proof

let z be object ; :: thesis: ( z in A implies not z in B )
assume z in A ; :: thesis: not z in B
then not z = y by A3, A5, TARSKI:def 1;
hence not z in B by A4, TARSKI:def 1; :: thesis: verum

end;

hence A misses B by XBOOLE_0:3; :: thesis: verum

end;

hence ( A = B or A misses B ) by A3, A4; :: thesis: verum

end;

take F ; :: thesis: ( union F = X & ( for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) ) )

now :: thesis: for y being object holds
( y in X iff ex Z being set st
( y in Z & Z in F ) )

let y be object ; :: thesis: ( y in X iff ex Z being set st
( y in Z & Z in F ) )

now :: thesis: ( y in X implies ex Z being set st
( y in Z & Z in F ) )

set Z = {y};
assume A6: y in X ; :: thesis: ex Z being set st
( y in Z & Z in F )
then {y} is Subset of X by ZFMISC_1:31;
then ( y in {y} & {y} in F ) by A1, A6, TARSKI:def 1;
hence ex Z being set st
( y in Z & Z in F ) ; :: thesis: verum

end;

hence ( y in X iff ex Z being set st
( y in Z & Z in F ) ) ; :: thesis: verum

end;

hence ( union F = X & ( for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) ) ) by A2, TARSKI:def 4; :: thesis: verum