let L be non empty Boolean RelStr ; :: thesis: for a, b, c being Element of L st a <= b "\/" c & a "/\" c = Bottom L holds
a <= b
let a, b, c be Element of L; :: thesis: ( a <= b "\/" c & a "/\" c = Bottom L implies a <= b )
assume that
A1: a <= b "\/" c and
A2: a "/\" c = Bottom L ; :: thesis: a <= b
A3: a "/\" (b "\/" c) = a by A1, Th10;
a "/\" (b "\/" c) = (a "/\" b) "\/" (Bottom L) by A2, WAYBEL_1:def 3;
then a "/\" b = a by A3, WAYBEL_1:4;
hence a <= b by YELLOW_0:23; :: thesis: verum