let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds a '&' b '<' a 'or' b
let a, b be Function of Y,BOOLEAN; :: thesis: a '&' b '<' a 'or' b
( a '&' b '<' a & a '<' a 'or' b ) by Lm1, Th38a;
hence a '&' b '<' a 'or' b by BVFUNC_1:15; :: thesis: verum