let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; :: thesis: ex c being Element of L st
for a being Element of L holds
( c + a = c & a + (a ` ) = c )
consider b being Element of L;
take c = (b ` ) + b; :: thesis: for a being Element of L holds
( c + a = c & a + (a ` ) = c )
let a be Element of L; :: 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