consider u being BinOp of (bool {} );
take /\-SemiLattStr(# (bool {} ),u #) ; :: thesis: ( /\-SemiLattStr(# (bool {} ),u #) is strict & not /\-SemiLattStr(# (bool {} ),u #) is empty )
thus ( /\-SemiLattStr(# (bool {} ),u #) is strict & not /\-SemiLattStr(# (bool {} ),u #) is empty ) ; :: thesis: verum