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 ( a <= b "\/" c & a "/\" c = Bottom L ) ; :: thesis: a <= b
then ( a "/\" (b "\/" c) = a & a "/\" (b "\/" c) = (a "/\" b) "\/" (Bottom L) ) by Th10, WAYBEL_1:def 3;
then a "/\" b = a by WAYBEL_1:3;
hence a <= b by YELLOW_0:23; :: thesis: verum