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