let L be lower-bounded Semilattice; :: thesis: for a, b, c being Element of L st a <= b & a <= c & b "/\" c = Bottom L holds
a = Bottom L
let a, b, c be Element of L; :: thesis: ( a <= b & a <= c & b "/\" c = Bottom L implies a = Bottom L )
assume that
A1: a <= b and
A2: a <= c and
A3: b "/\" c = Bottom L ; :: thesis: a = Bottom L
a "/\" c <= b "/\" c by A1, Th6;
then a <= b "/\" c by A2, Th10;
hence a = Bottom L by A3, Th19; :: thesis: verum