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