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

hereby :: thesis: ( x "/\" y = y implies [x,y] in ThetaOrder L )

assume [x,y] in ThetaOrder L ; :: thesis: x "/\" y = y
then consider a1, b1 being Element of L such that
A1: ( [x,y] = [a1,b1] & a1 "/\" b1 = b1 ) ;
thus x "/\" y = y by A1, XTUPLE_0:1; :: thesis: verum

end;

assume x "/\" y = y ; :: thesis: [x,y] in ThetaOrder L
hence [x,y] in ThetaOrder L ; :: thesis: verum