let uu, nn be BinOp of (bool {} ); :: thesis: for x, y being Element of LattStr(# (bool {} ),uu,nn #) holds x = y
let x, y be Element of LattStr(# (bool {} ),uu,nn #); :: thesis: x = y
x = {} ;
hence x = y ; :: thesis: verum