let T be TopStruct ; :: thesis: ( {} T is closed & [#] T is closed & ( for A, B being Subset of T st A is closed & B is closed holds
A \/ B is closed ) & ( for F being Subset-Family of T st F is closed holds
meet F is closed ) implies T is TopSpace )
assume that
A1: ( {} T is closed & [#] T is closed ) and
A2: for A, B being Subset of T st A is closed & B is closed holds
A \/ B is closed and
A3: for F being Subset-Family of T st F is closed holds
meet F is closed ; :: thesis: T is TopSpace
A4: the carrier of T in the topology of T

proof

([#] T) \ ({} T) is open by A1, PRE_TOPC:def 6;
hence the carrier of T in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

A5: for G being Subset-Family of T st G c= the topology of T holds
union G in the topology of T

proof

let G be Subset-Family of T; :: thesis: ( G c= the topology of T implies union G in the topology of T )
reconsider G' = G as Subset-Family of T ;
assume A6: G c= the topology of T ; :: thesis: union G in the topology of T

per cases ( G = {} or G <> {} ) ;

suppose A7: G = {} ; :: thesis: union G in the topology of T

([#] T) \ ({} T) = [#] T ;
then {} T is open by A1, Lm3;
hence union G in the topology of T by A7, PRE_TOPC:def 5, ZFMISC_1:2; :: thesis: verum

end;

suppose A8: G <> {} ; :: thesis: union G in the topology of T

A9: for A being Subset of T st A in G holds
([#] T) \ A is closed

proof

let A be Subset of T; :: thesis: ( A in G implies ([#] T) \ A is closed )
assume A in G ; :: thesis: ([#] T) \ A is closed
then A is open by A6, PRE_TOPC:def 5;
hence ([#] T) \ A is closed by Lm3; :: thesis: verum

end;

reconsider CG = COMPLEMENT G as Subset-Family of T ;
COMPLEMENT G is closed

proof

let A be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not A in COMPLEMENT G or A is closed )
assume A in COMPLEMENT G ; :: thesis: A is closed
then A ` in G' by SETFAM_1:def 8;
then ([#] T) \ (A ` ) is closed by A9;
hence A is closed by PRE_TOPC:22; :: thesis: verum

end;

then meet CG is closed by A3;
then (union G') ` is closed by A8, TOPS_2:11;
then ([#] T) \ (union G) is closed ;
then union G is open by Lm3;
hence union G in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

end;

end;

for A, B being Subset of T st A in the topology of T & B in the topology of T holds
A /\ B in the topology of T

proof

let A, B be Subset of T; :: thesis: ( A in the topology of T & B in the topology of T implies A /\ B in the topology of T )
assume that
A10: A in the topology of T and
A11: B in the topology of T ; :: thesis: A /\ B in the topology of T
reconsider A = A, B = B as Subset of T ;
A is open by A10, PRE_TOPC:def 5;
then A12: ([#] T) \ A is closed by Lm3;
B is open by A11, PRE_TOPC:def 5;
then ([#] T) \ B is closed by Lm3;
then (([#] T) \ A) \/ (([#] T) \ B) is closed by A2, A12;
then ([#] T) \ (A /\ B) is closed by XBOOLE_1:54;
then A /\ B is open by Lm3;
hence A /\ B in the topology of T by PRE_TOPC:def 5; :: thesis: verum

end;

hence T is TopSpace by A4, A5, PRE_TOPC:def 1; :: thesis: verum