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 Th22;
A2: d '&' (B_SUP a) = (B_SUP d) '&' (B_SUP a) by Th22;
A3: B_INF d = d by Th22;

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 Th5;
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, 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 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 Th5;
B_INF d = I_el Y by A6, Def13;
then d 'or' (B_INF a) = I_el Y by A1, Th10;
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, Th9;
A27: d = I_el Y by A3, A6, Def13;
A28: for x being Element of Y holds (d 'or' a) . x = TRUE by A27, Th10, Def11;
A33: 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, A33, A26, Def13, Th6; :: 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 A34: ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) ; :: thesis:

A35: now :: thesis:

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

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

A38: 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 A34, Def4;
hence (d 'or' a) . x = TRUE by A37; :: thesis:

end;

B_SUP d = O_el Y by A34, Def14;
then A39: d '&' (B_SUP a) = O_el Y by A2, Th5;
A40: 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 A34, MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A41: B_INF a = I_el Y by A37, Def13;
B_INF d = O_el Y by A34, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A41, 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 A38, A40, A39, Def13, Def14; :: thesis:

end;

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

A43: 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 A34, A42;
then (d 'or' a) . x = FALSE 'or' FALSE by Def4;
hence (d 'or' a) . x = FALSE ; :: thesis:

end;

A44: now :: thesis:

assume A45: 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 A43;
hence contradiction by A45; :: thesis:

end;

B_SUP d = O_el Y by A34, Def14;
then A46: d '&' (B_SUP a) = O_el Y by A2, Th5;
A47: 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 A34, A42;
then (d '&' a) . x = FALSE '&' FALSE by MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A48: B_INF a = O_el Y by A42, Def13;
B_INF d = O_el Y by A34, 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, A44, A47, A48, A46, Def13, Def14; :: thesis:

end;

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

A50: 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 A34, A49;
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 A34, Def14;
then A51: d '&' (B_SUP a) = O_el Y by A2, Th5;
A52: 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 A34, A49;
then (d '&' a) . x = FALSE '&' TRUE by MARGREL1:def 20;
hence (d '&' a) . x = FALSE ; :: thesis:

end;

A53: B_INF a = I_el Y by A49, Def13;
B_INF d = O_el Y by A34, Def13;
then d 'or' (B_INF a) = I_el Y by A1, A53, 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 A50, A52, A51, 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, A34, Def13;
hence (d '&' a) . x = FALSE by Def10, Th5; :: thesis:

end;

then A54: B_SUP (d '&' a) = O_el Y by Def14;
assume that
A55: 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 A34, Def13;
then A56: d 'or' (B_INF a) = (O_el Y) 'or' (O_el Y) by A1, A55, Def13;
A61: 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 A34;
hence (d 'or' a) . x = a . x ; :: thesis:

end;

B_SUP d = O_el Y by A34, 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, A55, A61, A54, A56, 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 A35; :: thesis:

end;

case A62: ( ( 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 A62;
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 A62; :: 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
A63: not for x being Element of Y holds d . x = TRUE and
A64: not for x being Element of Y holds d . x = FALSE ; :: thesis:

now :: thesis:

per cases by Th21;

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 A64, 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 A63, 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: