let B be Boolean Lattice; :: thesis: for x being Element of B
for xx being Element of (BA2TBA B) st xx = x holds
x ` = xx `
let x be Element of B; :: thesis: for xx being Element of (BA2TBA B) st xx = x holds
x ` = xx `
let xx be Element of (BA2TBA B); :: thesis: ( xx = x implies x ` = xx ` )
assume A1: xx = x ; :: thesis: x ` = xx `
xx ` = the Compl of (BA2TBA B) . xx by ROBBINS1:def 3
.= x ` by A1, LATTICE4:def 13 ;
hence x ` = xx ` ; :: thesis: verum