let X be set ; :: thesis:
let F be Subset-Family of X; :: thesis:
assume A1: {} in F ; :: thesis:
set O = COMPLEMENT F;
assume A2: for A, B being set st A in F & B in F holds
A \/ B in F ; :: thesis:
assume A3: for G being Subset-Family of X st G c= F holds
Intersect G in F ; :: thesis:
let T be TopStruct ; :: thesis:
assume that
A4: the carrier of T = X and
A5: the topology of T = COMPLEMENT F ; :: thesis:
T is TopSpace-like

({} 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:

hereby :: thesis:

let a be Subset-Family of T; :: thesis:
assume a c= the topology of T ; :: thesis:
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:

end;

let a, b be Subset of T; :: thesis:
assume that
A6: a in the topology of T and
A7: b in the topology of T ; :: thesis:
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:

end;

hence T is TopSpace ; :: thesis:
let A be Subset of T; :: thesis:
( 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: