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

hereby :: thesis: ( x [= y implies [x,y] in LatOrder L )

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

end;

assume x [= y ; :: thesis: [x,y] in LatOrder L
hence [x,y] in LatOrder L ; :: thesis: verum