let L be non empty Boolean RelStr ; :: thesis: for a, b, c being Element of L st a \ b <= c holds
a <= b "\/" c
let a, b, c be Element of L; :: thesis: ( a \ b <= c implies a <= b "\/" c )
A1: a <= a "\/" b by YELLOW_0:22;
assume a \ b <= c ; :: thesis: a <= b "\/" c
then A2: (a "/\" ('not' b)) "\/" b <= c "\/" b by Th7;
(a "/\" ('not' b)) "\/" b = (b "\/" a) "/\" (b "\/" ('not' b)) by Th17
.= (b "\/" a) "/\" (Top L) by Th34
.= a "\/" b by WAYBEL_1:4 ;
hence a <= b "\/" c by A2, A1, YELLOW_0:def 2; :: thesis: verum