thus
( T is normal implies for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds

ex P, Q being Subset of T st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) ; :: thesis: ( ( for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds

ex P, Q being Subset of T st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) implies T is normal )

assume A5: for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds

ex P, Q being Subset of T st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ; :: thesis: T is normal

let F1, F2 be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( not F1 is closed or not F2 is closed or not F1 misses F2 or ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & F1 c= b_{1} & F2 c= b_{2} & b_{1} misses b_{2} ) )

assume that

A6: F1 is closed and

A7: F2 is closed and

A8: F1 misses F2 ; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & F1 c= b_{1} & F2 c= b_{2} & b_{1} misses b_{2} )

ex P, Q being Subset of T st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) ; :: thesis: ( ( for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds

ex P, Q being Subset of T st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ) implies T is normal )

assume A5: for W, V being Subset of T st W <> {} & V <> {} & W is closed & V is closed & W misses V holds

ex P, Q being Subset of T st

( P is open & Q is open & W c= P & V c= Q & P misses Q ) ; :: thesis: T is normal

let F1, F2 be Subset of T; :: according to PRE_TOPC:def 12 :: thesis: ( not F1 is closed or not F2 is closed or not F1 misses F2 or ex b

( b

assume that

A6: F1 is closed and

A7: F2 is closed and

A8: F1 misses F2 ; :: thesis: ex b

( b

per cases
( F1 = {} or F2 = {} or ( F1 <> {} & F2 <> {} ) )
;

end;

suppose A9:
F1 = {}
; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & F1 c= b_{1} & F2 c= b_{2} & b_{1} misses b_{2} )

( b

take G1 = {} T; :: thesis: ex b_{1} being Element of bool the carrier of T st

( G1 is open & b_{1} is open & F1 c= G1 & F2 c= b_{1} & G1 misses b_{1} )

take G2 = [#] T; :: thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus ( G1 is open & G2 is open ) ; :: thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus F1 c= G1 by A9; :: thesis: ( F2 c= G2 & G1 misses G2 )

thus F2 c= G2 ; :: thesis: G1 misses G2

thus G1 misses G2 ; :: thesis: verum

end;( G1 is open & b

take G2 = [#] T; :: thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus ( G1 is open & G2 is open ) ; :: thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus F1 c= G1 by A9; :: thesis: ( F2 c= G2 & G1 misses G2 )

thus F2 c= G2 ; :: thesis: G1 misses G2

thus G1 misses G2 ; :: thesis: verum

suppose A10:
F2 = {}
; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & F1 c= b_{1} & F2 c= b_{2} & b_{1} misses b_{2} )

( b

take G1 = [#] T; :: thesis: ex b_{1} being Element of bool the carrier of T st

( G1 is open & b_{1} is open & F1 c= G1 & F2 c= b_{1} & G1 misses b_{1} )

take G2 = {} T; :: thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus ( G1 is open & G2 is open ) ; :: thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus F1 c= G1 ; :: thesis: ( F2 c= G2 & G1 misses G2 )

thus F2 c= G2 by A10; :: thesis: G1 misses G2

thus G1 misses G2 ; :: thesis: verum

end;( G1 is open & b

take G2 = {} T; :: thesis: ( G1 is open & G2 is open & F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus ( G1 is open & G2 is open ) ; :: thesis: ( F1 c= G1 & F2 c= G2 & G1 misses G2 )

thus F1 c= G1 ; :: thesis: ( F2 c= G2 & G1 misses G2 )

thus F2 c= G2 by A10; :: thesis: G1 misses G2

thus G1 misses G2 ; :: thesis: verum

suppose
( F1 <> {} & F2 <> {} )
; :: thesis: ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & F1 c= b_{1} & F2 c= b_{2} & b_{1} misses b_{2} )

( b

hence
ex b_{1}, b_{2} being Element of bool the carrier of T st

( b_{1} is open & b_{2} is open & F1 c= b_{1} & F2 c= b_{2} & b_{1} misses b_{2} )
by A5, A6, A7, A8; :: thesis: verum

end;( b