let L be non empty naturally_sup-generated LattRelStr ; :: thesis: for x, y being Element of L holds
( x <= y iff x [= y )
let x, y be Element of L; :: thesis: ( x <= y iff x [= y )

hereby :: thesis: ( x [= y implies x <= y )

assume x <= y ; :: thesis: x [= y
then x |_| y = y by Def10;
hence x [= y by LATTICES:def 3; :: thesis: verum

end;

assume x [= y ; :: thesis: x <= y
then x |_| y = y by LATTICES:def 3;
hence x <= y by Def10; :: thesis: verum