let Y be non empty set ; :: thesis:
let d be constant Element of Funcs (Y,BOOLEAN); :: thesis:

A1: now

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

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 Def14;
hence ( B_INF d = d & B_SUP d = d ) by A3, Def16, Def17; :: 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 Def13;
hence ( B_INF d = d & B_SUP d = d ) by A4, Def16, Def17; :: 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

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

per cases by Th24;

case d = O_el Y ; :: thesis:

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

end;

case d = I_el Y ; :: thesis:

hence ( B_INF d = d & B_SUP d = d ) by A6, Def14; :: 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: