let L be non empty Boolean RelStr ; :: thesis: for a, b, c being Element of L st a <= b holds
c \ b <= c \ a
let a, b, c be Element of L; :: thesis: ( a <= b implies c \ b <= c \ a )
assume a <= b ; :: thesis: c \ b <= c \ a
then 'not' b <= 'not' a by Th40;
then c "/\" ('not' b) <= c "/\" ('not' a) by Th6;
hence c \ b <= c \ a ; :: thesis: verum