let L be WA-Lattice; :: thesis: 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 ) )
let a, b, x be Element of L; :: thesis: ( not x in Segment (a,b) or ( a <= x & x <= b ) or ( b <= x & x <= a ) )
assume x in Segment (a,b) ; :: thesis: ( ( a <= x & x <= b ) or ( b <= x & x <= a ) )
then consider xx being Element of L such that
D1: ( x = xx & ( ( a <= xx & xx <= b ) or ( b <= xx & xx <= a ) ) ) ;
thus ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) by D1; :: thesis: verum