let Y be non empty set ; :: thesis: for a being Element of Funcs (Y,BOOLEAN)
for d being constant Element of Funcs (Y,BOOLEAN) holds
( 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 )
let a be Element of Funcs (Y,BOOLEAN); :: thesis: for d being constant Element of Funcs (Y,BOOLEAN) holds
( 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 )
let d be constant Element of Funcs (Y,BOOLEAN); :: thesis: ( 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 )
A1: d 'or' (B_INF a) = (B_INF d) 'or' (B_INF a) by Th25;
A2: d '&' (B_SUP a) = (B_SUP d) '&' (B_SUP a) by Th25;
A3: B_INF d = d by Th25;

A4: now

assume A5: ( for x being Element of Y holds d . x = TRUE or for x being Element of Y holds d . x = FALSE ) ; :: thesis: ( 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 )

now

per cases ( ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE ) or ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE ) or ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) ) ) 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: ( 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 )

A7: now

assume A8: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; :: thesis: ( 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 )

now

per cases ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ) 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: ( 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 )

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

proof

let x be Element of Y; :: thesis: (d '&' a) . x = TRUE
( 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: verum

end;

A11: now

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

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 = TRUE
( (d 'or' a) . x = (d . x) 'or' (a . x) & a . x = TRUE ) by A9, Def7;
hence (d 'or' a) . x = TRUE ; :: thesis: verum

end;

A14: ( B_INF a = I_el Y & B_SUP a = I_el Y ) by A9, Def16, Def17;
( B_INF d = I_el Y & B_SUP d = I_el Y ) by A6, Def16, Def17;
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, Def16, Def17; :: thesis: verum

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: ( 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 )

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

proof

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

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 = TRUE
( (d 'or' a) . x = (d . x) 'or' (a . x) & d . x = TRUE ) by A6, Def7;
hence (d 'or' a) . x = TRUE ; :: thesis: verum

end;

B_SUP a = O_el Y by A15, Def17;
then A18: d '&' (B_SUP a) = O_el Y by Th8;
A19: B_INF a = O_el Y by A15, Def16;
B_INF d = I_el Y by A6, Def16;
then d 'or' (B_INF a) = I_el Y by A1, A19, Th12;
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, Def16, Def17; :: thesis: verum

end;

case A20: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; :: thesis: ( 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 )

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

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
( 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: verum

end;

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

proof

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

end;

B_SUP a = O_el Y by A20, Def17;
then A23: d '&' (B_SUP a) = O_el Y by Th8;
B_INF d = I_el Y by A6, Def16;
then d 'or' (B_INF a) = I_el Y by A1, Th13;
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, Def16, Def17; :: thesis: verum

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: verum

end;

now

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: ( 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 )
A25: B_INF a = O_el Y by A24, Def16;
B_INF d = I_el Y by A6, Def16;
then A26: d 'or' (B_INF a) = I_el Y by A1, A25, Th12;
A27: d = I_el Y by A3, A6, Def16;
A28: for x being Element of Y holds (d 'or' a) . x = TRUE

proof

let x be Element of Y; :: thesis: (d 'or' a) . x = TRUE
(d 'or' a) . x = (I_el Y) . x by A27, Th13;
hence (d 'or' a) . x = TRUE by Def14; :: thesis: verum

end;

consider k4 being Function such that
A29: a = k4 and
A30: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A31: d '&' a = k3 and
A32: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds (d '&' a) . x = a . x

proof

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

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A31, A29;
then A33: B_SUP (d '&' a) = B_SUP a by A31, A32, A29, A30, FUNCT_1:2;
B_SUP d = I_el Y by A6, Def17;
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, Def16, Th9; :: thesis: verum

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: verum

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: ( 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 )

A35: now

assume A36: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; :: thesis: ( 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 )

now

per cases ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ) 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: ( 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 )

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

end;

B_SUP d = O_el Y by A34, Def17;
then A39: d '&' (B_SUP a) = O_el Y by A2, Th8;
A40: for x being Element of Y holds (d '&' a) . x = FALSE

proof

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

end;

A41: B_INF a = I_el Y by A37, Def16;
B_INF d = O_el Y by A34, Def16;
then d 'or' (B_INF a) = I_el Y by A1, A41, Th12;
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, Def16, Def17; :: thesis: verum

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: ( 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 )

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

proof

let x be Element of Y; :: thesis: (d 'or' a) . x = FALSE
( d . x = FALSE & a . x = FALSE ) by A34, A42;
then (d 'or' a) . x = FALSE 'or' FALSE by Def7;
hence (d 'or' a) . x = FALSE ; :: thesis: verum

end;

A44: now

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

end;

B_SUP d = O_el Y by A34, Def17;
then A46: d '&' (B_SUP a) = O_el Y by A2, Th8;
A47: for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
( 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: verum

end;

A48: B_INF a = O_el Y by A42, Def16;
B_INF d = O_el Y by A34, Def16;
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, Def16, Def17; :: thesis: verum

end;

case A49: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; :: thesis: ( 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 )

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

proof

let x be Element of Y; :: thesis: (d 'or' a) . x = TRUE
( d . x = FALSE & a . x = TRUE ) by A34, A49;
then (d 'or' a) . x = FALSE 'or' TRUE by Def7;
hence (d 'or' a) . x = TRUE ; :: thesis: verum

end;

B_SUP d = O_el Y by A34, Def17;
then A51: d '&' (B_SUP a) = O_el Y by A2, Th8;
A52: for x being Element of Y holds (d '&' a) . x = FALSE

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
( 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: verum

end;

A53: B_INF a = I_el Y by A49, Def16;
B_INF d = O_el Y by A34, Def16;
then d 'or' (B_INF a) = I_el Y by A1, A53, Th12;
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, Def16, Def17; :: thesis: verum

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: verum

end;

now

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

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
(d '&' a) . x = ((O_el Y) '&' a) . x by A3, A34, Def16;
then (d '&' a) . x = (O_el Y) . x by Th8;
hence (d '&' a) . x = FALSE by Def13; :: thesis: verum

end;

then A54: B_SUP (d '&' a) = O_el Y by Def17;
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 'or' a) = d 'or' (B_INF a) & B_SUP (d '&' a) = d '&' (B_SUP a) & B_SUP (a '&' d) = (B_SUP a) '&' d )
B_INF d = O_el Y by A34, Def16;
then A56: d 'or' (B_INF a) = (O_el Y) 'or' (O_el Y) by A1, A55, Def16;
consider k4 being Function such that
A57: a = k4 and
A58: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A59: d 'or' a = k3 and
A60: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds (d 'or' a) . x = a . x

proof

let x be Element of Y; :: thesis: (d 'or' a) . x = a . x
(d 'or' a) . x = (d . x) 'or' (a . x) by Def7;
then (d 'or' a) . x = FALSE 'or' (a . x) by A34;
hence (d 'or' a) . x = a . x ; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A59, A57;
then A61: k3 = k4 by A60, A58, FUNCT_1:2;
B_SUP d = O_el Y by A34, Def17;
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, A59, A57, A61, A54, A56, Def16, Th8; :: thesis: verum

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: verum

end;

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

let x be Element of Y; :: thesis: ( 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 )
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: verum

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: verum

end;

now

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: ( 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 )

now

per cases ( d = O_el Y or d = I_el Y ) by Th24;

case d = O_el Y ; :: thesis: ( 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 )

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, Def13; :: thesis: verum

end;

case d = I_el Y ; :: thesis: ( 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 )

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, Def14; :: thesis: verum

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: verum

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: verum