let L be non empty join-commutative \/-SemiLattStr ; :: thesis: for a, b being Element of L st a [= b & b [= a holds
a = b
let a, b be Element of L; :: thesis: ( a [= b & b [= a implies a = b )
assume ( a "\/" b = b & b "\/" a = a ) ; :: according to LATTICES:def 3 :: thesis: a = b
hence a = b ; :: thesis: verum