let L be non empty LattRelStr ; :: thesis: ( L is join-commutative & L is naturally_sup-generated implies L is antisymmetric )
assume ( L is join-commutative & L is naturally_sup-generated ) ; :: thesis: L is antisymmetric
then reconsider L9 = L as non empty join-commutative naturally_sup-generated LattRelStr ;
for x, y being Element of L9 st x <= y & y <= x holds
x = y
proof
let x, y be Element of L9; :: thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; :: thesis: x = y
then ( x [= y & y [= x ) by Th22;
hence x = y by LATTICES:8; :: thesis: verum
end;
hence L is antisymmetric by YELLOW_0:def 3; :: thesis: verum