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
A1: a '&' b '<' a by Lm1;
a '<' a 'or' b by Th39;
hence a '&' b '<' a 'or' b by A1, BVFUNC_1:18; :: thesis: verum