theorem :: BVFUNC_6:139

for Y being non empty set
for a, b, c, d being Function of Y,BOOLEAN st a '<' b & c '<' d holds
a 'or' c '<' b 'or' d