theorem ThetaOrdLat: :: LATTAD_1:29

for L being GAD_Lattice
for x, y being Element of L holds
( [x,y] in ThetaOrder L iff x "/\" y = y )