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 = ((( the Element of L `) + the Element of L) + (a `)) ` by Th3
.= (((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