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