let X be set ; :: thesis: for F being Subset-Family of X st {} in F & ( for A, B being set st A in F & B in F holds

A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds

Intersect G in F ) holds

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

let F be Subset-Family of X; :: thesis: ( {} in F & ( for A, B being set st A in F & B in F holds

A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds

Intersect G in F ) implies for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

assume A1: {} in F ; :: thesis: ( ex A, B being set st

( A in F & B in F & not A \/ B in F ) or ex G being Subset-Family of X st

( G c= F & not Intersect G in F ) or for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

set O = COMPLEMENT F;

assume A2: for A, B being set st A in F & B in F holds

A \/ B in F ; :: thesis: ( ex G being Subset-Family of X st

( G c= F & not Intersect G in F ) or for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

assume A3: for G being Subset-Family of X st G c= F holds

Intersect G in F ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = COMPLEMENT F implies ( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

assume that

A4: the carrier of T = X and

A5: the topology of T = COMPLEMENT F ; :: thesis: ( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

T is TopSpace-like

( A is closed iff A in F )

let A be Subset of T; :: thesis: ( A is closed iff A in F )

( A is closed iff A ` is open ) ;

then ( A is closed iff A ` in COMPLEMENT F ) by A5;

hence ( A is closed iff A in F ) by A4, SETFAM_1:35; :: thesis: verum

A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds

Intersect G in F ) holds

for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

let F be Subset-Family of X; :: thesis: ( {} in F & ( for A, B being set st A in F & B in F holds

A \/ B in F ) & ( for G being Subset-Family of X st G c= F holds

Intersect G in F ) implies for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

assume A1: {} in F ; :: thesis: ( ex A, B being set st

( A in F & B in F & not A \/ B in F ) or ex G being Subset-Family of X st

( G c= F & not Intersect G in F ) or for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

set O = COMPLEMENT F;

assume A2: for A, B being set st A in F & B in F holds

A \/ B in F ; :: thesis: ( ex G being Subset-Family of X st

( G c= F & not Intersect G in F ) or for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

assume A3: for G being Subset-Family of X st G c= F holds

Intersect G in F ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = COMPLEMENT F holds

( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = COMPLEMENT F implies ( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) ) )

assume that

A4: the carrier of T = X and

A5: the topology of T = COMPLEMENT F ; :: thesis: ( T is TopSpace & ( for A being Subset of T holds

( A is closed iff A in F ) ) )

T is TopSpace-like

proof

hence
T is TopSpace
; :: thesis: for A being Subset of T holds
({} T) ` in COMPLEMENT F
by A1, A4, SETFAM_1:35;

hence the carrier of T in the topology of T by A5; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b_{1} being Element of bool (bool the carrier of T) holds

( not b_{1} c= the topology of T or union b_{1} in the topology of T ) ) & ( for b_{1}, b_{2} being Element of bool the carrier of T holds

( not b_{1} in the topology of T or not b_{2} in the topology of T or b_{1} /\ b_{2} in the topology of T ) ) )

assume that

A6: a in the topology of T and

A7: b in the topology of T ; :: thesis: a /\ b in the topology of T

A8: b ` in F by A7, A4, A5, SETFAM_1:def 7;

a ` in F by A6, A4, A5, SETFAM_1:def 7;

then (a `) \/ (b `) in F by A8, A2;

then (a /\ b) ` in F by XBOOLE_1:54;

hence a /\ b in the topology of T by A4, A5, SETFAM_1:def 7; :: thesis: verum

end;hence the carrier of T in the topology of T by A5; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b

( not b

( not b

hereby :: thesis: for b_{1}, b_{2} being Element of bool the carrier of T holds

( not b_{1} in the topology of T or not b_{2} in the topology of T or b_{1} /\ b_{2} in the topology of T )

let a, b be Subset of T; :: thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )( not b

let a be Subset-Family of T; :: thesis: ( a c= the topology of T implies union a in the topology of T )

assume a c= the topology of T ; :: thesis: union a in the topology of T

then COMPLEMENT a c= F by A4, A5, SETFAM_1:37;

then Intersect (COMPLEMENT a) in F by A3, A4;

then (union a) ` in F by YELLOW_8:6;

hence union a in the topology of T by A4, A5, SETFAM_1:def 7; :: thesis: verum

end;assume a c= the topology of T ; :: thesis: union a in the topology of T

then COMPLEMENT a c= F by A4, A5, SETFAM_1:37;

then Intersect (COMPLEMENT a) in F by A3, A4;

then (union a) ` in F by YELLOW_8:6;

hence union a in the topology of T by A4, A5, SETFAM_1:def 7; :: thesis: verum

assume that

A6: a in the topology of T and

A7: b in the topology of T ; :: thesis: a /\ b in the topology of T

A8: b ` in F by A7, A4, A5, SETFAM_1:def 7;

a ` in F by A6, A4, A5, SETFAM_1:def 7;

then (a `) \/ (b `) in F by A8, A2;

then (a /\ b) ` in F by XBOOLE_1:54;

hence a /\ b in the topology of T by A4, A5, SETFAM_1:def 7; :: thesis: verum

( A is closed iff A in F )

let A be Subset of T; :: thesis: ( A is closed iff A in F )

( A is closed iff A ` is open ) ;

then ( A is closed iff A ` in COMPLEMENT F ) by A5;

hence ( A is closed iff A in F ) by A4, SETFAM_1:35; :: thesis: verum