let n be BinOp of (bool {}); :: thesis: for x, y being Element of \/-SemiLattStr(# (bool {}),n #) holds x = y
let x, y be Element of \/-SemiLattStr(# (bool {}),n #); :: thesis: x = y
x = {} ;
hence x = y ; :: thesis: verum