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

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