let L be non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ; :: thesis: ex c being Element of st
for a being Element of holds
( c + a = c & a + (a ` ) = c )
consider b being Element of ;
take c = (b ` ) + b; :: thesis: for a being Element of holds
( c + a = c & a + (a ` ) = c )
let a be Element of ; :: thesis: ( c + a = c & a + (a ` ) = c )
thus c + a = ((a ` ) + a) + a by Th4
.= (a ` ) + (a + a) by LATTICES:def 5
.= (a ` ) + a by Def7
.= c by Th4 ; :: thesis: a + (a ` ) = c
thus a + (a ` ) = c by Th4; :: thesis: verum