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 b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) )
assume that
A6: F1 is closed and
A7: F2 is closed and
A8: F1 misses F2 ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
per cases ( F1 = {} or F2 = {} or ( F1 <> {} & F2 <> {} ) ) ;
suppose A9: F1 = {} ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
take G1 = {} T; :: thesis: ex b1 being Element of bool the carrier of T st
( G1 is open & b1 is open & F1 c= G1 & F2 c= b1 & G1 misses b1 )
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;
suppose A10: F2 = {} ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
take G1 = [#] T; :: thesis: ex b1 being Element of bool the carrier of T st
( G1 is open & b1 is open & F1 c= G1 & F2 c= b1 & G1 misses b1 )
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;
suppose ( F1 <> {} & F2 <> {} ) ; :: thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 )
hence ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & F1 c= b1 & F2 c= b2 & b1 misses b2 ) by A5, A6, A7, A8; :: thesis: verum
end;
end;