consider u, n being BinOp of bool {} ;
take LattStr(# (bool {} ),u,n #) ; :: thesis: ( LattStr(# (bool {} ),u,n #) is strict & not LattStr(# (bool {} ),u,n #) is empty )
thus ( LattStr(# (bool {} ),u,n #) is strict & not LattStr(# (bool {} ),u,n #) is empty ) ; :: thesis: verum