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 )
now
per cases ( B <> [#] T or B = [#] T ) ;
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 )
reconsider W = Cl A, V = ([#] T) \ B as Subset of T ;
A5: ( W <> {} & V <> {} )
proof
A6: ([#] T) \ B <> {}
proof
assume ([#] T) \ B = {} ; :: thesis: contradiction
then B = ([#] T) \ {} by PRE_TOPC:3;
hence contradiction by A4; :: thesis: verum
end;
A c= Cl A by PRE_TOPC:18;
hence ( W <> {} & V <> {} ) by A2, A6; :: thesis: verum
end;
A7: W misses V
proof
assume W meets V ; :: thesis: contradiction
then consider x being set 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;
B = ([#] T) \ V by PRE_TOPC:3;
then V is closed by PRE_TOPC:def 3;
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, A5, A7, COMPTS_1:def 3;
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
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;
hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) by A9; :: thesis: verum
end;
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 )
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;
end;
end;
hence ex C being Subset of T st
( C <> {} & C is open & Cl A c= C & Cl C c= B ) ; :: thesis: verum