let L be 1 -element /\-SemiLattStr ; :: 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 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 STRUCT_0:def 10; :: thesis: verum