defpred S_{1}[ 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_{1}[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 ) ) )

( A <> {} & ( for B being Subset of X holds

( not B in F or A = B or A misses B ) ) ) ) )

( 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

( 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

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

take
F
; :: thesis: ( union F = X & ( for A being Subset of X st A in F holds
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;

end;( 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 )

hence
( A = B or A misses B )
by A3, A4; :: thesis: verumassume A5:
not x = y
; :: thesis: A misses B

for z being object st z in A holds

not z in B

end;for z being object st z in A holds

not z in B

proof

hence
A misses B
by XBOOLE_0:3; :: thesis: verum
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;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

( 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 ) )

hence
( union F = X & ( for A being Subset of X st A in F 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 ) )

( y in Z & Z in F ) ) ; :: thesis: verum

end;( y in Z & Z in F ) )

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

( y in Z & Z in F ) )

hence
( y in X iff 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;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

( y in Z & Z in F ) ) ; :: thesis: verum

( 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