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
A4: b "/\" c = Bottom L by A3, Def3;
A5: Bottom L <= a "/\" c by YELLOW_0:44;
a "/\" c <= Bottom L by A1, A4, Th6;
then a "/\" c = Bottom L by A5, YELLOW_0:def 3;
hence a = Bottom L by A2, Th10; :: thesis: verum