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