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 and

A2: [#] T is closed and

A3: for A, B being Subset of T st A is closed & B is closed holds

A \/ B is closed and

A4: for F being Subset-Family of T st F is closed holds

meet F is closed ; :: thesis: T is TopSpace

A5: 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

union G in the topology of T

then the carrier of T in the topology of T by PRE_TOPC:def 2;

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

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 and

A2: [#] T is closed and

A3: for A, B being Subset of T st A is closed & B is closed holds

A \/ B is closed and

A4: for F being Subset-Family of T st F is closed holds

meet F is closed ; :: thesis: T is TopSpace

A5: 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

A9:
for G being Subset-Family of T st G c= the topology of T holds
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

A6: A in the topology of T and

A7: B in the topology of T ; :: thesis: A /\ B in the topology of T

reconsider A = A, B = B as Subset of T ;

B is open by A7, PRE_TOPC:def 2;

then A8: ([#] T) \ B is closed by Lm2;

A is open by A6, PRE_TOPC:def 2;

then ([#] T) \ A is closed by Lm2;

then (([#] T) \ A) \/ (([#] T) \ B) is closed by A3, A8;

then ([#] T) \ (A /\ B) is closed by XBOOLE_1:54;

then A /\ B is open by Lm2;

hence A /\ B in the topology of T by PRE_TOPC:def 2; :: thesis: verum

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

reconsider A = A, B = B as Subset of T ;

B is open by A7, PRE_TOPC:def 2;

then A8: ([#] T) \ B is closed by Lm2;

A is open by A6, PRE_TOPC:def 2;

then ([#] T) \ A is closed by Lm2;

then (([#] T) \ A) \/ (([#] T) \ B) is closed by A3, A8;

then ([#] T) \ (A /\ B) is closed by XBOOLE_1:54;

then A /\ B is open by Lm2;

hence A /\ B in the topology of T by PRE_TOPC:def 2; :: thesis: verum

union G in the topology of T

proof

([#] T) \ ({} T) is open
by A1, PRE_TOPC:def 3;
let G be Subset-Family of T; :: thesis: ( G c= the topology of T implies union G in the topology of T )

reconsider G9 = G as Subset-Family of T ;

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

end;reconsider G9 = G as Subset-Family of T ;

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

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

end;

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

([#] T) \ ({} T) = [#] T
;

then {} T is open by A2, Lm2;

hence union G in the topology of T by A11, PRE_TOPC:def 2, ZFMISC_1:2; :: thesis: verum

end;then {} T is open by A2, Lm2;

hence union G in the topology of T by A11, PRE_TOPC:def 2, ZFMISC_1:2; :: thesis: verum

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

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

A13: for A being Subset of T st A in G holds

([#] T) \ A is closed by A10, Lm2, PRE_TOPC:def 2;

COMPLEMENT G is closed

then (union G9) ` is closed by A12, TOPS_2:6;

then ([#] T) \ (union G) is closed ;

then union G is open by Lm2;

hence union G in the topology of T by PRE_TOPC:def 2; :: thesis: verum

end;A13: for A being Subset of T st A in G holds

([#] T) \ A is closed by A10, Lm2, PRE_TOPC:def 2;

COMPLEMENT G is closed

proof

then
meet CG is closed
by A4;
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 G9 by SETFAM_1:def 7;

then ([#] T) \ (A `) is closed by A13;

hence A is closed by PRE_TOPC:3; :: thesis: verum

end;assume A in COMPLEMENT G ; :: thesis: A is closed

then A ` in G9 by SETFAM_1:def 7;

then ([#] T) \ (A `) is closed by A13;

hence A is closed by PRE_TOPC:3; :: thesis: verum

then (union G9) ` is closed by A12, TOPS_2:6;

then ([#] T) \ (union G) is closed ;

then union G is open by Lm2;

hence union G in the topology of T by PRE_TOPC:def 2; :: thesis: verum

then the carrier of T in the topology of T by PRE_TOPC:def 2;

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