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