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
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
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;
A9: 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 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 <> {} ) ;
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
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 G9 by SETFAM_1:def 7;
then ([#] T) \ (A `) is closed by A13;
hence A is closed by PRE_TOPC:3; :: thesis: verum
end;
then meet CG is closed by A4;
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;
end;
end;
([#] T) \ ({} T) is open by A1, PRE_TOPC:def 3;
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