theorem :: LATTAD_1:50

for L being GAD_Lattice
for a, b being Element of L
for x, y being Element of (LatRelStr L) st a = x & b = y holds
( x <= y iff a [= b ) by OrdLat, ORDERS_2:def 5;