let L be WA_Lattice; :: thesis: for x, y being Element of L
for xx, yy being Element of (LatRelStr L) st x = xx & y = yy holds
( x [= y iff xx <= yy )
let x, y be Element of L; :: thesis: for xx, yy being Element of (LatRelStr L) st x = xx & y = yy holds
( x [= y iff xx <= yy )
let xx, yy be Element of (LatRelStr L); :: thesis: ( x = xx & y = yy implies ( x [= y iff xx <= yy ) )
assume A1: ( x = xx & y = yy ) ; :: thesis: ( x [= y iff xx <= yy )
thus ( x [= y implies xx <= yy ) :: thesis: ( xx <= yy implies x [= y )

proof

assume x [= y ; :: thesis: xx <= yy
then [xx,yy] in LatOrder L by A1;
hence xx <= yy by ORDERS_2:def 5; :: thesis: verum

end;

assume xx <= yy ; :: thesis: x [= y
then [xx,yy] in the InternalRel of (LatRelStr L) by ORDERS_2:def 5;
hence x [= y by A1, Idem2; :: thesis: verum