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 )
set b = the Element of L;
take c = ( the Element of L `) + the Element of L; :: 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