let L be WA_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: ( [a1,b1] = [x,y] & a1 [= b1 ) ;
( a1 = x & b1 = y ) by A1, XTUPLE_0:1;
hence x [= y by A1; :: thesis: verum

end;

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