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