let L be non empty \/-SemiLattStr ; :: thesis: ( L is trivial implies ( L is join-commutative & L is join-associative ) )
assume A1: L is trivial ; :: 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 A1, 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 A1, STRUCT_0:def 10; :: thesis: verum