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

A1: now

assume not for x being Element of Y holds a . x = FALSE ; :: thesis: a . x <= (B_SUP a) . x
then B_SUP a = I_el Y by Def17;
then (B_SUP a) . x = TRUE by Def14;
then (a . x) => ((B_SUP a) . x) = TRUE ;
hence a . x <= (B_SUP a) . x by Def3; :: thesis: verum

end;

now

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

end;

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