let T be complete continuous TopLattice; :: thesis: ( T is Lawson implies T is T_2 )
assume A1: T is Lawson ; :: thesis: T is T_2
let x, y be Point of T; :: according to PRE_TOPC:def 16 :: 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 x' = x, y' = 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 y' <= x' or not x' <= y' ) by A2, ORDERS_2:25;

suppose not y' <= x' ; :: 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 << y' & not u <= x' ) 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 A4, YELLOW_9:1; :: thesis: ( y in W & V misses W )
thus y in W by A4; :: thesis: V misses W
( W c= uparrow u & V ` = uparrow u ) by WAYBEL_3:11;
hence V misses W by SUBSET_1:43; :: thesis: verum

end;

suppose not 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₂ )

then consider u being Element of T such that
A5: ( u << x' & not u <= y' ) 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 A5; :: thesis: ( y in V & W misses V )
thus y in V by A5, YELLOW_9:1; :: thesis: W misses V
( W c= uparrow u & V ` = uparrow u ) by WAYBEL_3:11;
hence W misses V by SUBSET_1:43; :: thesis: verum

end;

end;