let X be non empty TopSpace; :: thesis: ( X is normal iff for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) )

thus ( X is normal implies for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) ) :: thesis: ( ( for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) ) implies X is normal )

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) ; :: thesis: X is normal

for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds

ex G, H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H )

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) )

thus ( X is normal implies for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) ) :: thesis: ( ( for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) ) implies X is normal )

proof

assume A15:
for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds
assume A1:
for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds

ex G, H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H ) ; :: according to COMPTS_1:def 3 :: thesis: for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C )

let A, C be Subset of X; :: thesis: ( A <> {} & C <> [#] X & A c= C & A is closed & C is open implies ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) )

assume that

A2: A <> {} and

A3: C <> [#] X and

A4: A c= C and

A5: A is closed and

A6: C is open ; :: thesis: ex G being Subset of X st

( G is open & A c= G & Cl G c= C )

set B = ([#] X) \ C;

([#] X) \ C c= A ` by A4, XBOOLE_1:34;

then A7: A misses ([#] X) \ C by SUBSET_1:23;

( ([#] X) \ C <> {} & C ` is closed ) by A3, A6, PRE_TOPC:4;

then consider G, H being Subset of X such that

A8: G is open and

A9: H is open and

A10: A c= G and

A11: ([#] X) \ C c= H and

A12: G misses H by A1, A2, A5, A7;

take G ; :: thesis: ( G is open & A c= G & Cl G c= C )

for p being object st p in Cl G holds

p in C

end;ex G, H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H ) ; :: according to COMPTS_1:def 3 :: thesis: for A, C being Subset of X st A <> {} & C <> [#] X & A c= C & A is closed & C is open holds

ex G being Subset of X st

( G is open & A c= G & Cl G c= C )

let A, C be Subset of X; :: thesis: ( A <> {} & C <> [#] X & A c= C & A is closed & C is open implies ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) )

assume that

A2: A <> {} and

A3: C <> [#] X and

A4: A c= C and

A5: A is closed and

A6: C is open ; :: thesis: ex G being Subset of X st

( G is open & A c= G & Cl G c= C )

set B = ([#] X) \ C;

([#] X) \ C c= A ` by A4, XBOOLE_1:34;

then A7: A misses ([#] X) \ C by SUBSET_1:23;

( ([#] X) \ C <> {} & C ` is closed ) by A3, A6, PRE_TOPC:4;

then consider G, H being Subset of X such that

A8: G is open and

A9: H is open and

A10: A c= G and

A11: ([#] X) \ C c= H and

A12: G misses H by A1, A2, A5, A7;

take G ; :: thesis: ( G is open & A c= G & Cl G c= C )

for p being object st p in Cl G holds

p in C

proof

hence
( G is open & A c= G & Cl G c= C )
by A8, A10; :: thesis: verum
let p be object ; :: thesis: ( p in Cl G implies p in C )

assume A13: p in Cl G ; :: thesis: p in C

then reconsider y = p as Point of X ;

( H ` is closed & G c= H ` ) by A9, A12, SUBSET_1:23;

then A14: y in H ` by A13, PRE_TOPC:15;

H ` c= (([#] X) \ C) ` by A11, SUBSET_1:12;

then y in (([#] X) \ C) ` by A14;

hence p in C by PRE_TOPC:3; :: thesis: verum

end;assume A13: p in Cl G ; :: thesis: p in C

then reconsider y = p as Point of X ;

( H ` is closed & G c= H ` ) by A9, A12, SUBSET_1:23;

then A14: y in H ` by A13, PRE_TOPC:15;

H ` c= (([#] X) \ C) ` by A11, SUBSET_1:12;

then y in (([#] X) \ C) ` by A14;

hence p in C by PRE_TOPC:3; :: thesis: verum

ex G being Subset of X st

( G is open & A c= G & Cl G c= C ) ; :: thesis: X is normal

for A, B being Subset of X st A <> {} & B <> {} & A is closed & B is closed & A misses B holds

ex G, H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H )

proof

hence
X is normal
; :: thesis: verum
let A, B be Subset of X; :: thesis: ( A <> {} & B <> {} & A is closed & B is closed & A misses B implies ex G, H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H ) )

assume that

A16: A <> {} and

A17: B <> {} and

A18: A is closed and

A19: ( B is closed & A misses B ) ; :: thesis: ex G, H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H )

set C = ([#] X) \ B;

([#] X) \ (([#] X) \ B) = B by PRE_TOPC:3;

then A20: ([#] X) \ B <> [#] X by A17, PRE_TOPC:4;

( A c= B ` & ([#] X) \ B is open ) by A19, PRE_TOPC:def 3, SUBSET_1:23;

then consider G being Subset of X such that

A21: G is open and

A22: A c= G and

A23: Cl G c= ([#] X) \ B by A15, A16, A18, A20;

take G ; :: thesis: ex H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H )

take H = ([#] X) \ (Cl G); :: thesis: ( G is open & H is open & A c= G & B c= H & G misses H )

thus ( G is open & H is open ) by A21, PRE_TOPC:def 3; :: thesis: ( A c= G & B c= H & G misses H )

(([#] X) \ B) ` c= (Cl G) ` by A23, SUBSET_1:12;

hence ( A c= G & B c= H ) by A22, PRE_TOPC:3; :: thesis: G misses H

H c= G ` by PRE_TOPC:18, XBOOLE_1:34;

hence G misses H by SUBSET_1:23; :: thesis: verum

end;( G is open & H is open & A c= G & B c= H & G misses H ) )

assume that

A16: A <> {} and

A17: B <> {} and

A18: A is closed and

A19: ( B is closed & A misses B ) ; :: thesis: ex G, H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H )

set C = ([#] X) \ B;

([#] X) \ (([#] X) \ B) = B by PRE_TOPC:3;

then A20: ([#] X) \ B <> [#] X by A17, PRE_TOPC:4;

( A c= B ` & ([#] X) \ B is open ) by A19, PRE_TOPC:def 3, SUBSET_1:23;

then consider G being Subset of X such that

A21: G is open and

A22: A c= G and

A23: Cl G c= ([#] X) \ B by A15, A16, A18, A20;

take G ; :: thesis: ex H being Subset of X st

( G is open & H is open & A c= G & B c= H & G misses H )

take H = ([#] X) \ (Cl G); :: thesis: ( G is open & H is open & A c= G & B c= H & G misses H )

thus ( G is open & H is open ) by A21, PRE_TOPC:def 3; :: thesis: ( A c= G & B c= H & G misses H )

(([#] X) \ B) ` c= (Cl G) ` by A23, SUBSET_1:12;

hence ( A c= G & B c= H ) by A22, PRE_TOPC:3; :: thesis: G misses H

H c= G ` by PRE_TOPC:18, XBOOLE_1:34;

hence G misses H by SUBSET_1:23; :: thesis: verum