let T be complete continuous TopLattice; :: thesis:
assume A1: T is Lawson ; :: thesis:
let x, y be Point of T; :: according to PRE_TOPC:def 10 :: thesis:
assume A2: x <> y ; :: thesis:
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 by A2, ORDERS_2:2;

suppose not y9 <= x9 ; :: thesis:

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:
take W = wayabove u; :: thesis:
thus ( V is open & W is open ) by A1, Th39, Th40; :: thesis:
thus x in V by A5, YELLOW_9:1; :: thesis:
thus y in W by A4; :: thesis:
A6: V ` = uparrow u ;
W c= uparrow u by WAYBEL_3:11;
hence V misses W by A6, SUBSET_1:23; :: thesis:

end;

suppose not x9 <= y9 ; :: thesis:

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:
take V = (uparrow u) ` ; :: thesis:
thus ( W is open & V is open ) by A1, Th39, Th40; :: thesis:
thus x in W by A7; :: thesis:
thus y in V by A8, YELLOW_9:1; :: thesis:
A9: V ` = uparrow u ;
W c= uparrow u by WAYBEL_3:11;
hence W misses V by A9, SUBSET_1:23; :: thesis:

end;

end;