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

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