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

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