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