let L be non empty Boolean RelStr ; :: thesis: for a, b, c, d being Element of L st a <= b & c <= d holds
a \ d <= b \ c
let a, b, c, d be Element of L; :: thesis: ( a <= b & c <= d implies a \ d <= b \ c )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: a \ d <= b \ c
'not' d <= 'not' c by A2, Th37;
then A3: a "/\" ('not' d) <= a "/\" ('not' c) by Th6;
a "/\" ('not' c) <= b "/\" ('not' c) by A1, Th6;
hence a \ d <= b \ c by A3, YELLOW_0:def 2; :: thesis: verum