theorem :: LATWAL_2:39
for L being WA-Lattice
for a, b, x being Element of L holds
( not x in Segment (a,b) or ( a <= x & x <= b ) or ( b <= x & x <= a ) )