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 = {} & y = {} ) ;
hence x = y ; :: thesis: verum