let L be non empty /\-SemiLattStr ; :: thesis: ( L is trivial implies ( L is meet-commutative & L is meet-associative ) )
assume A2: L is trivial ; :: thesis: ( L is meet-commutative & L is meet-associative )
thus L is meet-commutative :: thesis: L is meet-associative

proof

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

end;

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