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