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 = (((b ` ) + b) + (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