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:
assume A in F ; :: thesis:
then consider x being object such that
x in X and
A3: A = {x} by A1;
thus A <> {} by A3; :: thesis:
let B be Subset of X; :: thesis:
assume B in F ; :: thesis:
then consider y being object such that
y in X and
A4: B = {y} by A1;

now :: thesis:

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

proof

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

end;

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

end;

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

end;

take F ; :: thesis:

now :: thesis:

let y be object ; :: thesis:

now :: thesis:

set Z = {y};
assume A6: y in X ; :: thesis:
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:

end;

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

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: