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 )

set a = the Element of L;
assume A1: IT = Top L ; :: thesis: ex a being Element of L st IT = a + (a `)
take a = the Element of L; :: 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