let Y be non empty set ; :: thesis: for a, b, c, d being Element of Funcs Y,BOOLEAN st a '<' b & c '<' d holds
a 'or' c '<' b 'or' d
let a, b, c, d be Element of Funcs Y,BOOLEAN ; :: thesis: ( a '<' b & c '<' d implies a 'or' c '<' b 'or' d )
assume ( a '<' b & c '<' d ) ; :: thesis: a 'or' c '<' b 'or' d
then ( a 'imp' b = I_el Y & c 'imp' d = I_el Y ) by BVFUNC_1:19;
then (a 'or' c) 'imp' (b 'or' d) = I_el Y by BVFUNC_6:22;
hence a 'or' c '<' b 'or' d by BVFUNC_1:19; :: thesis: verum