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