let l be Lattice; :: thesis: for b being Element of l st ( for a being Element of l holds a "\/" b = b ) holds
b = Top l
let b be Element of l; :: thesis: ( ( for a being Element of l holds a "\/" b = b ) implies b = Top l )
assume A1: for a being Element of l holds a "\/" b = b ; :: thesis: b = Top l
then for a being Element of l holds
( b "\/" a = b & a "\/" b = b ) ;
then l is upper-bounded ;
hence Top l = (Top l) "\/" b
.= b by A1 ;
:: thesis: verum