let T be non empty TopSpace; :: thesis: ( T is normal implies for A, B being open Subset of T st A <> {} & Cl A c= B holds

ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) )

assume A1: T is normal ; :: thesis: for A, B being open Subset of T st A <> {} & Cl A c= B holds

ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

let A, B be open Subset of T; :: thesis: ( A <> {} & Cl A c= B implies ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) )

assume that

A2: A <> {} and

A3: Cl A c= B ; :: thesis: ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

( C <> {} & C is open & Cl A c= C & Cl C c= B ) ; :: thesis: verum

ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) )

assume A1: T is normal ; :: thesis: for A, B being open Subset of T st A <> {} & Cl A c= B holds

ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

let A, B be open Subset of T; :: thesis: ( A <> {} & Cl A c= B implies ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) )

assume that

A2: A <> {} and

A3: Cl A c= B ; :: thesis: ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

now :: thesis: ( ( B <> [#] T & ex C, C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) ) or ( B = [#] T & ex C, C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) ) )end;

hence
ex C being Subset of T st ( C <> {} & C is open & Cl A c= C & Cl C c= B ) ) or ( B = [#] T & ex C, C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) ) )

per cases
( B <> [#] T or B = [#] T )
;

end;

case A4:
B <> [#] T
; :: thesis: ex C, C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

( C <> {} & C is open & Cl A c= C & Cl C c= B )

reconsider W = Cl A, V = ([#] T) \ B as Subset of T ;

A5: ( W <> {} & V <> {} )

then V is closed ;

then consider C, Q being Subset of T such that

A9: C is open and

A10: Q is open and

A11: W c= C and

A12: V c= Q and

A13: C misses Q by A1, A7;

take C = C; :: thesis: ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

( C <> {} & Cl A c= C & Cl C c= B )

( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A9; :: thesis: verum

end;A5: ( W <> {} & V <> {} )

proof

A7:
W misses V
A6:
([#] T) \ B <> {}

hence ( W <> {} & V <> {} ) by A2, A6; :: thesis: verum

end;proof

A c= Cl A
by PRE_TOPC:18;
assume
([#] T) \ B = {}
; :: thesis: contradiction

then B = ([#] T) \ {} by PRE_TOPC:3;

hence contradiction by A4; :: thesis: verum

end;then B = ([#] T) \ {} by PRE_TOPC:3;

hence contradiction by A4; :: thesis: verum

hence ( W <> {} & V <> {} ) by A2, A6; :: thesis: verum

proof

B = ([#] T) \ V
by PRE_TOPC:3;
assume
W meets V
; :: thesis: contradiction

then consider x being object such that

A8: x in W /\ V by XBOOLE_0:4;

( x in Cl A & x in ([#] T) \ B ) by A8, XBOOLE_0:def 4;

hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum

end;then consider x being object such that

A8: x in W /\ V by XBOOLE_0:4;

( x in Cl A & x in ([#] T) \ B ) by A8, XBOOLE_0:def 4;

hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum

then V is closed ;

then consider C, Q being Subset of T such that

A9: C is open and

A10: Q is open and

A11: W c= C and

A12: V c= Q and

A13: C misses Q by A1, A7;

take C = C; :: thesis: ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

( C <> {} & Cl A c= C & Cl C c= B )

proof

hence
ex C being Subset of T st
consider Q0, C0 being Subset of ([#] T) such that

A14: ( Q0 = Q & C0 = C ) ;

C0 c= Q0 ` by A13, A14, SUBSET_1:23;

then Cl C c= Q ` by A10, A14, TOPS_1:5;

then Cl C misses Q by SUBSET_1:23;

then A15: V misses Cl C by A12, XBOOLE_1:63;

(B `) ` = B ;

hence ( C <> {} & Cl A c= C & Cl C c= B ) by A5, A11, A15, SUBSET_1:23; :: thesis: verum

end;A14: ( Q0 = Q & C0 = C ) ;

C0 c= Q0 ` by A13, A14, SUBSET_1:23;

then Cl C c= Q ` by A10, A14, TOPS_1:5;

then Cl C misses Q by SUBSET_1:23;

then A15: V misses Cl C by A12, XBOOLE_1:63;

(B `) ` = B ;

hence ( C <> {} & Cl A c= C & Cl C c= B ) by A5, A11, A15, SUBSET_1:23; :: thesis: verum

( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A9; :: thesis: verum

case A16:
B = [#] T
; :: thesis: ex C, C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

( C <> {} & C is open & Cl A c= C & Cl C c= B )

consider C being Subset of T such that

A17: C = [#] T ;

take C = C; :: thesis: ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

Cl C c= B by A16;

hence ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A17; :: thesis: verum

end;A17: C = [#] T ;

take C = C; :: thesis: ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B )

Cl C c= B by A16;

hence ex C being Subset of T st

( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A17; :: thesis: verum

( C <> {} & C is open & Cl A c= C & Cl C c= B ) ; :: thesis: verum