set u = the BinOp of (bool {});
take GGm = /\-SemiLattStr(# (bool {}), the BinOp of (bool {}) #); :: thesis: ( GGm is strict & GGm is meet-commutative & GGm is meet-associative )
( ( for x, y being Element of GGm holds x "/\" y = y "/\" x ) & ( 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 ) ; :: thesis: verum