theorem Th22: :: ROBBINS3:22

for L being non empty naturally_sup-generated LattRelStr
for x, y being Element of L holds
( x <= y iff x [= y ) by Def10;