consider u being BinOp of (bool {} );
take GGj = \/-SemiLattStr(# (bool {} ),u #); :: thesis: ( GGj is strict & GGj is join-commutative & GGj is join-associative )
A1: for x, y being Element of GGj holds x "\/" y = y "\/" x by Lm2;
for x, y, z being Element of GGj holds x "\/" (y "\/" z) = (x "\/" y) "\/" z by Lm2;
hence ( GGj is strict & GGj is join-commutative & GGj is join-associative ) by A1, Def4, Def5; :: thesis: verum