let Y be non empty set ; :: thesis: for a being Element of Funcs (Y,BOOLEAN)
for x being Element of Y holds (B_INF a) . x <= a . x
let a be Element of Funcs (Y,BOOLEAN); :: thesis: for x being Element of Y holds (B_INF a) . x <= a . x
let x be Element of Y; :: thesis: (B_INF a) . x <= a . x

A1: now

assume not for x being Element of Y holds a . x = TRUE ; :: thesis: (B_INF a) . x <= a . x
then B_INF a = O_el Y by Def16;
then (B_INF a) . x = FALSE by Def13;
then ((B_INF a) . x) => (a . x) = TRUE ;
hence (B_INF a) . x <= a . x by Def3; :: thesis: verum

end;

now

assume for x being Element of Y holds a . x = TRUE ; :: thesis: (B_INF a) . x <= a . x
then a . x = TRUE ;
then ((B_INF a) . x) => (a . x) = TRUE ;
hence (B_INF a) . x <= a . x by Def3; :: thesis: verum

end;

hence (B_INF a) . x <= a . x by A1; :: thesis: verum