let L be non empty Boolean RelStr ; :: thesis: for a, b, c being Element of L st a <= b "\/" c holds

( a \ b <= c & a \ c <= b )

let a, b, c be Element of L; :: thesis: ( a <= b "\/" c implies ( a \ b <= c & a \ c <= b ) )

assume A1: a <= b "\/" c ; :: thesis: ( a \ b <= c & a \ c <= b )

(b "\/" c) "/\" ('not' b) = (('not' b) "/\" b) "\/" (('not' b) "/\" c) by WAYBEL_1:def 3

.= (Bottom L) "\/" (('not' b) "/\" c) by Th34

.= c "/\" ('not' b) by WAYBEL_1:3 ;

then ( c "/\" ('not' b) <= c & a "/\" ('not' b) <= c "/\" ('not' b) ) by A1, Th6, YELLOW_0:23;

hence a \ b <= c by YELLOW_0:def 2; :: thesis: a \ c <= b

(b "\/" c) "/\" ('not' c) = (('not' c) "/\" b) "\/" (('not' c) "/\" c) by WAYBEL_1:def 3

.= (('not' c) "/\" b) "\/" (Bottom L) by Th34

.= ('not' c) "/\" b by WAYBEL_1:3 ;

then ( ('not' c) "/\" b <= b & a "/\" ('not' c) <= ('not' c) "/\" b ) by A1, Th6, YELLOW_0:23;

hence a \ c <= b by YELLOW_0:def 2; :: thesis: verum

( a \ b <= c & a \ c <= b )

let a, b, c be Element of L; :: thesis: ( a <= b "\/" c implies ( a \ b <= c & a \ c <= b ) )

assume A1: a <= b "\/" c ; :: thesis: ( a \ b <= c & a \ c <= b )

(b "\/" c) "/\" ('not' b) = (('not' b) "/\" b) "\/" (('not' b) "/\" c) by WAYBEL_1:def 3

.= (Bottom L) "\/" (('not' b) "/\" c) by Th34

.= c "/\" ('not' b) by WAYBEL_1:3 ;

then ( c "/\" ('not' b) <= c & a "/\" ('not' b) <= c "/\" ('not' b) ) by A1, Th6, YELLOW_0:23;

hence a \ b <= c by YELLOW_0:def 2; :: thesis: a \ c <= b

(b "\/" c) "/\" ('not' c) = (('not' c) "/\" b) "\/" (('not' c) "/\" c) by WAYBEL_1:def 3

.= (('not' c) "/\" b) "\/" (Bottom L) by Th34

.= ('not' c) "/\" b by WAYBEL_1:3 ;

then ( ('not' c) "/\" b <= b & a "/\" ('not' c) <= ('not' c) "/\" b ) by A1, Th6, YELLOW_0:23;

hence a \ c <= b by YELLOW_0:def 2; :: thesis: verum