let Y be non empty set ; :: thesis: ( B_INF (O_el Y) = O_el Y & B_INF (I_el Y) = I_el Y & B_SUP (O_el Y) = O_el Y & B_SUP (I_el Y) = I_el Y )
A1: not for x being Element of Y holds (O_el Y) . x = TRUE
proof
now :: thesis: ( ( for x being Element of Y holds (O_el Y) . x = TRUE ) implies for x being Element of Y holds
not for x being Element of Y holds (O_el Y) . x = TRUE )
assume for x being Element of Y holds (O_el Y) . x = TRUE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds (O_el Y) . x = TRUE
let x be Element of Y; :: thesis: not for x being Element of Y holds (O_el Y) . x = TRUE
(O_el Y) . x = FALSE by Def10;
hence not for x being Element of Y holds (O_el Y) . x = TRUE ; :: thesis: verum
end;
hence not for x being Element of Y holds (O_el Y) . x = TRUE ; :: thesis: verum
end;
A2: not for x being Element of Y holds (I_el Y) . x = FALSE
proof
now :: thesis: ( ( for x being Element of Y holds (I_el Y) . x = FALSE ) implies for x being Element of Y holds
not for x being Element of Y holds (I_el Y) . x = FALSE )
assume A3: for x being Element of Y holds (I_el Y) . x = FALSE ; :: thesis: for x being Element of Y holds
not for x being Element of Y holds (I_el Y) . x = FALSE
let x be Element of Y; :: thesis: not for x being Element of Y holds (I_el Y) . x = FALSE
(I_el Y) . x = FALSE by A3;
hence not for x being Element of Y holds (I_el Y) . x = FALSE by Def11; :: thesis: verum
end;
hence not for x being Element of Y holds (I_el Y) . x = FALSE ; :: thesis: verum
end;
( ( for x being Element of Y holds (O_el Y) . x = FALSE ) & ( for x being Element of Y holds (I_el Y) . x = TRUE ) ) by Def10, Def11;
hence ( B_INF (O_el Y) = O_el Y & B_INF (I_el Y) = I_el Y & B_SUP (O_el Y) = O_el Y & B_SUP (I_el Y) = I_el Y ) by A1, A2, Def13, Def14; :: thesis: verum