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: B_INF d = d by Th25;
A2: d 'or' (B_INF a) = (B_INF d) 'or' (B_INF a) by Th25;
A3: d '&' (B_SUP a) = (B_SUP d) '&' (B_SUP a) 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 'or' a) . x = TRUE

proof

let x be Element of Y; :: thesis: (d 'or' a) . x = TRUE
A11: (d 'or' a) . x = (d . x) 'or' (a . x) by Def7;
a . x = TRUE by A9;
hence (d 'or' a) . x = TRUE by A11; :: thesis: verum

end;

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

proof

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

end;

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

proof

now

assume A15: 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 A12;
hence contradiction by A15; :: thesis: verum

end;

hence not for x being Element of Y holds (d '&' a) . x = FALSE ; :: thesis: verum

end;

A16: B_INF d = I_el Y by A6, Def16;
A17: B_SUP d = I_el Y by A6, Def17;
A18: B_INF a = I_el Y by A9, Def16;
B_SUP a = I_el Y by A9, 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, A3, A10, A14, A16, A17, A18, Def16, Def17; :: thesis: verum

end;

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

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

end;

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

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
A23: (d '&' a) . x = (d . x) '&' (a . x) by MARGREL1:def 21;
a . x = FALSE by A19;
hence (d '&' a) . x = FALSE by A23; :: thesis: verum

end;

A24: B_INF d = I_el Y by A6, Def16;
A25: B_INF a = O_el Y by A19, Def16;
A26: B_SUP a = O_el Y by A19, Def17;
A27: d 'or' (B_INF a) = I_el Y by A2, A24, A25, Th12;
d '&' (B_SUP a) = O_el Y by A26, 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 A20, A22, A27, Def16, Def17; :: thesis: verum

end;

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

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

end;

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

proof

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

end;

A33: B_INF d = I_el Y by A6, Def16;
A34: B_SUP a = O_el Y by A28, Def17;
A35: d 'or' (B_INF a) = I_el Y by A2, A33, Th13;
d '&' (B_SUP a) = O_el Y by A34, 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 A29, A31, A35, 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 A36: ( not 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 )
A37: B_INF d = I_el Y by A6, Def16;
A38: B_SUP d = I_el Y by A6, Def17;
A39: B_INF a = O_el Y by A36, Def16;
A40: d = I_el Y by A1, A6, Def16;
A41: 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 A40, Th13;
hence (d 'or' a) . x = TRUE by Def14; :: thesis: verum

end;

A42: 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 A40, MARGREL1:def 21;
then (d '&' a) . x = TRUE '&' (a . x) by Def14;
hence (d '&' a) . x = a . x ; :: thesis: verum

end;

consider k3 being Function such that
A43: ( d '&' a = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A44: ( a = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A42, A43, A44;
then A45: B_SUP (d '&' a) = B_SUP a by A43, A44, FUNCT_1:9;
d 'or' (B_INF a) = I_el Y by A2, A37, A39, 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 A3, A38, A41, A45, 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 A46: ( ( 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 )

A47: now

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

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

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

end;

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

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
A53: (d '&' a) . x = (d . x) '&' (a . x) by MARGREL1:def 21;
d . x = FALSE by A46;
hence (d '&' a) . x = FALSE by A53; :: thesis: verum

end;

A54: B_INF d = O_el Y by A46, Def16;
A55: B_SUP d = O_el Y by A46, Def17;
B_INF a = I_el Y by A49, Def16;
then A56: d 'or' (B_INF a) = I_el Y by A2, A54, Th12;
d '&' (B_SUP a) = O_el Y by A3, A55, 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 A50, A52, A56, Def16, Def17; :: thesis: verum

end;

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

A58: 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
A59: d . x = FALSE by A46;
a . x = FALSE by A57;
then (d 'or' a) . x = FALSE 'or' FALSE by A59, Def7;
hence (d 'or' a) . x = FALSE ; :: thesis: verum

end;

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

proof

now

assume A61: 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 A58;
hence contradiction by A61; :: thesis: verum

end;

hence not for x being Element of Y holds (d 'or' a) . x = TRUE ; :: thesis: verum

end;

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

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
A63: d . x = FALSE by A46;
a . x = FALSE by A57;
then (d '&' a) . x = FALSE '&' FALSE by A63, MARGREL1:def 21;
hence (d '&' a) . x = FALSE ; :: thesis: verum

end;

A64: B_INF d = O_el Y by A46, Def16;
A65: B_SUP d = O_el Y by A46, Def17;
A66: B_INF a = O_el Y by A57, Def16;
d '&' (B_SUP a) = O_el Y by A3, A65, 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 A2, A60, A62, A64, A66, Def16, Def17; :: thesis: verum

end;

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

A68: 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
A69: d . x = FALSE by A46;
a . x = TRUE by A67;
then (d 'or' a) . x = FALSE 'or' TRUE by A69, Def7;
hence (d 'or' a) . x = TRUE ; :: thesis: verum

end;

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

proof

let x be Element of Y; :: thesis: (d '&' a) . x = FALSE
A71: d . x = FALSE by A46;
a . x = TRUE by A67;
then (d '&' a) . x = FALSE '&' TRUE by A71, MARGREL1:def 21;
hence (d '&' a) . x = FALSE ; :: thesis: verum

end;

A72: B_INF d = O_el Y by A46, Def16;
A73: B_SUP d = O_el Y by A46, Def17;
B_INF a = I_el Y by A67, Def16;
then A74: d 'or' (B_INF a) = I_el Y by A2, A72, Th12;
d '&' (B_SUP a) = O_el Y by A3, A73, 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 A68, A70, A74, 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 A75: ( not 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 )
A76: 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 A46;
hence (d 'or' a) . x = a . x ; :: thesis: verum

end;

consider k3 being Function such that
A77: ( d 'or' a = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A78: ( a = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
for u being set st u in Y holds
k3 . u = k4 . u by A76, A77, A78;
then A79: k3 = k4 by A77, A78, FUNCT_1:9;
A80: 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 A1, A46, Def16;
then (d '&' a) . x = (O_el Y) . x by Th8;
hence (d '&' a) . x = FALSE by Def13; :: thesis: verum

end;

A81: B_INF d = O_el Y by A46, Def16;
A82: B_SUP d = O_el Y by A46, Def17;
A83: B_SUP (d '&' a) = O_el Y by A80, Def17;
d 'or' (B_INF a) = (O_el Y) 'or' (O_el Y) by A2, A75, A81, 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 A3, A75, A77, A78, A79, A82, A83, 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 A47; :: thesis: verum

end;

case A84: ( ( 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 A84;
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 A84; :: 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 A85: ( not 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 )

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 A85, 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 A85, 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