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