consider u being BinOp of (bool {} );
take GGm = /\-SemiLattStr(# (bool {} ),u #); :: thesis: ( GGm is strict & GGm is meet-commutative & GGm is meet-associative )
A2: for x, y being Element of GGm holds x "/\" y = y "/\" x by Lm3;
for x, y, z being Element of GGm holds x "/\" (y "/\" z) = (x "/\" y) "/\" z by Lm3;
hence ( GGm is strict & GGm is meet-commutative & GGm is meet-associative ) by A2, Def6, Def7; :: thesis: verum