let T be complete continuous TopLattice; :: thesis: ( T is Lawson implies T is Hausdorff )
assume A1: T is Lawson ; :: thesis: T is Hausdorff
let x, y be Point of T; :: according to PRE_TOPC:def 10 :: thesis: ( x = y or ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & x in b₁ & y in b₂ & b₁ misses b₂ ) )
assume A2: x <> y ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & x in b₁ & y in b₂ & b₁ misses b₂ )
reconsider x9 = x, y9 = y as Element of T ;
A3: for x being Element of T holds
( not waybelow x is empty & waybelow x is directed ) ;

per cases ( not y9 <= x9 or not x9 <= y9 ) by A2, ORDERS_2:2;

suppose not y9 <= x9 ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & x in b₁ & y in b₂ & b₁ misses b₂ )

then consider u being Element of T such that
A4: u << y9 and
A5: not u <= x9 by A3, WAYBEL_3:24;
take V = (uparrow u) ` ; :: thesis: ex b<sub>1</sub> being Element of bool the carrier of T st
( V is open & b<sub>1</sub> is open & x in V & y in b<sub>1</sub> & V misses b<sub>1</sub> )
take W = wayabove u; :: thesis: ( V is open & W is open & x in V & y in W & V misses W )
thus ( V is open & W is open ) by A1, Th39, Th40; :: thesis: ( x in V & y in W & V misses W )
thus x in V by A5, YELLOW_9:1; :: thesis: ( y in W & V misses W )
thus y in W by A4; :: thesis: V misses W
A6: V ` = uparrow u ;
W c= uparrow u by WAYBEL_3:11;
hence V misses W by A6, SUBSET_1:23; :: thesis: verum

end;

suppose not x9 <= y9 ; :: thesis: ex b₁, b₂ being Element of bool the carrier of T st
( b₁ is open & b₂ is open & x in b₁ & y in b₂ & b₁ misses b₂ )

then consider u being Element of T such that
A7: u << x9 and
A8: not u <= y9 by A3, WAYBEL_3:24;
take W = wayabove u; :: thesis: ex b₁ being Element of bool the carrier of T st
( W is open & b₁ is open & x in W & y in b₁ & W misses b₁ )
take V = (uparrow u) ` ; :: thesis: ( W is open & V is open & x in W & y in V & W misses V )
thus ( W is open & V is open ) by A1, Th39, Th40; :: thesis: ( x in W & y in V & W misses V )
thus x in W by A7; :: thesis: ( y in V & W misses V )
thus y in V by A8, YELLOW_9:1; :: thesis: W misses V
A9: V ` = uparrow u ;
W c= uparrow u by WAYBEL_3:11;
hence W misses V by A9, SUBSET_1:23; :: thesis: verum

end;

end;