let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for x being Element of Y holds a . x <= (B_SUP a) . x
let a be Function of 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 :: thesis: ( not for x being Element of Y holds a . x = FALSE implies a . x <= (B_SUP a) . x )
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 Def14;
then (B_SUP a) . x = TRUE by Def11;
then (a . x) => ((B_SUP a) . x) = TRUE ;
hence a . x <= (B_SUP a) . x ; :: thesis: verum
end;
now :: thesis: ( ( for x being Element of Y holds a . x = FALSE ) implies a . x <= (B_SUP a) . x )
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 ; :: thesis: verum
end;
hence a . x <= (B_SUP a) . x by A1; :: thesis: verum