:: deftheorem defines Segment LATWAL_2:def 2 :
for W being WA-Lattice
for a, b being Element of W holds Segment (a,b) = { x where x is Element of W : ( ( a <= x & x <= b ) or ( b <= x & x <= a ) ) } ;