let Y be non empty set ; :: thesis:
let d be constant Function of Y,BOOLEAN; :: thesis:

A1: now :: thesis:

assume A2: ( for x being Element of Y holds d . x = TRUE or for x being Element of Y holds d . x = FALSE ) ; :: thesis:

now :: thesis:

per cases by A2;

case A3: ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) ; :: thesis:

then d = I_el Y by Def11;
hence ( B_INF d = d & B_SUP d = d ) by A3, Def13, Def14; :: thesis:

end;

case A4: ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) ; :: thesis:

then d = O_el Y by Def10;
hence ( B_INF d = d & B_SUP d = d ) by A4, Def13, Def14; :: thesis:

end;

case A5: ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ; :: thesis:

let x be Element of Y; :: thesis:
d . x = TRUE by A5;
hence ( B_INF d = d & B_SUP d = d ) by A5; :: thesis:

end;

end;

end;

hence ( B_INF d = d & B_SUP d = d ) ; :: thesis:

end;

now :: thesis:

assume that
A6: not for x being Element of Y holds d . x = TRUE and
A7: not for x being Element of Y holds d . x = FALSE ; :: thesis:

now :: thesis:

per cases by Th20;

case d = O_el Y ; :: thesis:

hence ( B_INF d = d & B_SUP d = d ) by A7, Def10; :: thesis:

end;

case d = I_el Y ; :: thesis:

hence ( B_INF d = d & B_SUP d = d ) by A6, Def11; :: thesis:

end;

end;

end;

hence ( B_INF d = d & B_SUP d = d ) ; :: thesis:

end;

hence ( B_INF d = d & B_SUP d = d ) by A1; :: thesis: