let IT be Element of L; :: thesis: ( IT = Top L iff ex a being Element of L st IT = a + (a ` ) )

hereby :: thesis: ( ex a being Element of L st IT = a + (a ` ) implies IT = Top L )

assume A1: IT = Top L ; :: thesis: ex a being Element of L st IT = a + (a ` )
consider a being Element of L;
take a = a; :: thesis: IT = a + (a ` )
for b being Element of L holds
( (a + (a ` )) + b = a + (a ` ) & b + (a + (a ` )) = a + (a ` ) )

proof

let b be Element of L; :: thesis: ( (a + (a ` )) + b = a + (a ` ) & b + (a + (a ` )) = a + (a ` ) )
(a + (a ` )) + b = (b + (b ` )) + b by Th4
.= (b ` ) + (b + b) by LATTICES:def 5
.= (b ` ) + b by Def7
.= (a ` ) + a by Th4 ;
hence ( (a + (a ` )) + b = a + (a ` ) & b + (a + (a ` )) = a + (a ` ) ) ; :: thesis: verum

end;

hence IT = a + (a ` ) by A1, LATTICES:def 17; :: thesis: verum

end;

given a being Element of L such that A2: IT = a + (a ` ) ; :: thesis: IT = Top L
A3: for b being Element of L holds (a + (a ` )) + b = a + (a ` )

proof

let b be Element of L; :: thesis: (a + (a ` )) + b = a + (a ` )
(a + (a ` )) + b = (b + (b ` )) + b by Th4
.= (b ` ) + (b + b) by LATTICES:def 5
.= (b ` ) + b by Def7
.= (a ` ) + a by Th4 ;
hence (a + (a ` )) + b = a + (a ` ) ; :: thesis: verum

end;

then for b being Element of L holds b + (a + (a ` )) = a + (a ` ) ;
hence IT = Top L by A2, A3, LATTICES:def 17; :: thesis: verum