let Y be non empty set ; :: thesis:
let a be Function of Y,BOOLEAN; :: thesis:
let d be constant Function of Y,BOOLEAN; :: thesis:
A1: d 'or' (B_INF a) = (B_INF d) 'or' (B_INF a) by Th21;
A2: d '&' (B_SUP a) = (B_SUP d) '&' (B_SUP a) by Th21;
A3: B_INF d = d by Th21;

A4: now :: thesis:

assume A5: ( 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 A5;

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

A7: now :: thesis:

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

now :: thesis:

per cases by A8;

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

A10: for x being Element of Y holds (d '&' a) . x = TRUE

proof

let x be Element of Y; :: thesis:
( d . x = TRUE & a . x = TRUE ) by A6, A9;
then (d '&' a) . x = TRUE '&' TRUE by MARGREL1:def 20;
hence (d '&' a) . x = TRUE ; :: thesis:

end;

A11: now :: thesis:

assume A12: for x being Element of Y holds (d '&' a) . x = FALSE ; :: thesis:
let x be Element of Y; :: thesis:
(d '&' a) . x = TRUE by A10;
hence contradiction by A12; :: thesis:

end;

A13: for x being Element of Y holds (d 'or' a) . x = TRUE

proof

let x be Element of Y; :: thesis:
( (d 'or' a) . x = (d . x) 'or' (a . x) & a . x = TRUE ) by A9, Def4;
hence (d 'or' a) . x = TRUE ; :: thesis:

end;

A14: ( B_INF a = I_el Y & B_SUP a = I_el Y ) by A9, Def13, Def14;
( B_INF d = I_el Y & B_SUP d = I_el Y ) by A6, Def13, Def14;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A1, A2, A13, A11, A14, Def13, Def14; :: thesis:

end;

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

A16: for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis:
( (d '&' a) . x = (d . x) '&' (a . x) & a . x = FALSE ) by A15, MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A17: for x being Element of Y holds (d 'or' a) . x = TRUE

proof

let x be Element of Y; :: thesis:
( (d 'or' a) . x = (d . x) 'or' (a . x) & d . x = TRUE ) by A6, Def4;
hence (d 'or' a) . x = TRUE ; :: thesis:

end;

B_SUP a = O_el Y by A15, Def14;
then A18: d '&' (B_SUP a) = O_el Y by Th4;
A19: B_INF a = O_el Y by A15, Def13;
B_INF d = I_el Y by A6, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A19, Th8;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A17, A16, A18, Def13, Def14; :: thesis:

end;

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

A21: for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis:
( d . x = TRUE & a . x = FALSE ) by A6, A20;
then (d '&' a) . x = TRUE '&' FALSE by MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A22: for x being Element of Y holds (d 'or' a) . x = TRUE

proof

let x be Element of Y; :: thesis:
( d . x = TRUE & a . x = FALSE ) by A6, A20;
then (d 'or' a) . x = TRUE 'or' FALSE by Def4;
hence (d 'or' a) . x = TRUE ; :: thesis:

end;

B_SUP a = O_el Y by A20, Def14;
then A23: d '&' (B_SUP a) = O_el Y by Th4;
B_INF d = I_el Y by A6, Def13;
then d 'or' (B_INF a) = I_el Y by A1, Th9;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A22, A21, A23, Def13, Def14; :: thesis:

end;

end;

end;

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; :: thesis:

end;

now :: thesis:

assume that
A24: not for x being Element of Y holds a . x = TRUE and
not for x being Element of Y holds a . x = FALSE ; :: thesis:
A25: B_INF a = O_el Y by A24, Def13;
B_INF d = I_el Y by A6, Def13;
then A26: d 'or' (B_INF a) = I_el Y by A1, A25, Th8;
A27: d = I_el Y by A3, A6, Def13;
A28: for x being Element of Y holds (d 'or' a) . x = TRUE by A27, Th9, Def11;
A29: d '&' a = a

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis:
(d '&' a) . x = ((I_el Y) . x) '&' (a . x) by A27, MARGREL1:def 20;
then (d '&' a) . x = TRUE '&' (a . x) by Def11;
hence (d '&' a) . x = a . x ; :: thesis:

end;

B_SUP d = I_el Y by A6, Def14;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A2, A28, A29, A26, Def13, Th5; :: thesis:

end;

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A7; :: thesis:

end;

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

A31: now :: thesis:

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

now :: thesis:

per cases by A32;

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

A34: for x being Element of Y holds (d 'or' a) . x = TRUE

proof

let x be Element of Y; :: thesis:
( (d 'or' a) . x = (d . x) 'or' (a . x) & d . x = FALSE ) by A30, Def4;
hence (d 'or' a) . x = TRUE by A33; :: thesis:

end;

B_SUP d = O_el Y by A30, Def14;
then A35: d '&' (B_SUP a) = O_el Y by A2, Th4;
A36: for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis:
( (d '&' a) . x = (d . x) '&' (a . x) & d . x = FALSE ) by A30, MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A37: B_INF a = I_el Y by A33, Def13;
B_INF d = O_el Y by A30, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A37, Th8;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A34, A36, A35, Def13, Def14; :: thesis:

end;

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

A39: for x being Element of Y holds (d 'or' a) . x = FALSE

proof

let x be Element of Y; :: thesis:
( d . x = FALSE & a . x = FALSE ) by A30, A38;
then (d 'or' a) . x = FALSE 'or' FALSE by Def4;
hence (d 'or' a) . x = FALSE ; :: thesis:

end;

A40: now :: thesis:

assume A41: for x being Element of Y holds (d 'or' a) . x = TRUE ; :: thesis:
let x be Element of Y; :: thesis:
(d 'or' a) . x = FALSE by A39;
hence contradiction by A41; :: thesis:

end;

B_SUP d = O_el Y by A30, Def14;
then A42: d '&' (B_SUP a) = O_el Y by A2, Th4;
A43: for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis:
( d . x = FALSE & a . x = FALSE ) by A30, A38;
then (d '&' a) . x = FALSE '&' FALSE by MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A44: B_INF a = O_el Y by A38, Def13;
B_INF d = O_el Y by A30, Def13;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A1, A40, A43, A44, A42, Def13, Def14; :: thesis:

end;

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

A46: for x being Element of Y holds (d 'or' a) . x = TRUE

proof

let x be Element of Y; :: thesis:
( d . x = FALSE & a . x = TRUE ) by A30, A45;
then (d 'or' a) . x = FALSE 'or' TRUE by Def4;
hence (d 'or' a) . x = TRUE ; :: thesis:

end;

B_SUP d = O_el Y by A30, Def14;
then A47: d '&' (B_SUP a) = O_el Y by A2, Th4;
A48: for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis:
( d . x = FALSE & a . x = TRUE ) by A30, A45;
then (d '&' a) . x = FALSE '&' TRUE by MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A49: B_INF a = I_el Y by A45, Def13;
B_INF d = O_el Y by A30, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A49, Th8;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A46, A48, A47, Def13, Def14; :: thesis:

end;

end;

end;

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; :: thesis:

end;

now :: thesis:

for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis:
(d '&' a) . x = ((O_el Y) '&' a) . x by A3, A30, Def13;
hence (d '&' a) . x = FALSE by Def10, Th4; :: thesis:

end;

then A50: B_SUP (d '&' a) = O_el Y by Def14;
assume that
A51: not for x being Element of Y holds a . x = TRUE and
not for x being Element of Y holds a . x = FALSE ; :: thesis:
B_INF d = O_el Y by A30, Def13;
then A52: d 'or' (B_INF a) = (O_el Y) 'or' (O_el Y) by A1, A51, Def13;
A53: d 'or' a = a

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis:
(d 'or' a) . x = (d . x) 'or' (a . x) by Def4;
then (d 'or' a) . x = FALSE 'or' (a . x) by A30;
hence (d 'or' a) . x = a . x ; :: thesis:

end;

B_SUP d = O_el Y by A30, Def14;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A2, A51, A53, A50, A52, Def13, Th4; :: thesis:

end;

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A31; :: thesis:

end;

case A54: ( ( 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 = FALSE by A54;
hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A54; :: thesis:

end;

end;

end;

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; :: thesis:

end;

now :: thesis:

assume that
A55: not for x being Element of Y holds d . x = TRUE and
A56: 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 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A56, Def10; :: thesis:

end;

case d = I_el Y ; :: thesis:

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A55, Def11; :: thesis:

end;

end;

end;

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) ; :: thesis:

end;

hence ( B_INF (d 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d ) by A4; :: thesis: