let L be 1 -element \/-SemiLattStr ; :: thesis: ( L is join-commutative & L is join-associative )
thus L is join-commutative :: thesis: L is join-associative

proof

let x, y be Element of L; :: according to LATTICES:def 4 :: thesis: x "\/" y = y "\/" x
thus x "\/" y = y "\/" x by STRUCT_0:def 10; :: thesis: verum

end;

let x, y, z be Element of L; :: according to LATTICES:def 5 :: thesis: x "\/" (y "\/" z) = (x "\/" y) "\/" z
thus x "\/" (y "\/" z) = (x "\/" y) "\/" z by STRUCT_0:def 10; :: thesis: verum