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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
let a be Element of Funcs (Y,BOOLEAN); :: thesis: for d being constant Element of Funcs (Y,BOOLEAN) holds
( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
let d be constant Element of Funcs (Y,BOOLEAN); :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
consider k3 being Function such that
A1: (I_el Y) 'imp' (I_el Y) = k3 and
A2: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A3: I_el Y = k4 and
A4: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds ((I_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x

proof

let x be Element of Y; :: thesis: ((I_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x
(I_el Y) . x = TRUE by Def14;
then ((I_el Y) 'imp' (I_el Y)) . x = ('not' TRUE) 'or' TRUE by Def11;
hence ((I_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x by Def14; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A1, A3;
then A5: (I_el Y) 'imp' (I_el Y) = I_el Y by A1, A2, A3, A4, FUNCT_1:9;
A6: (B_SUP a) 'imp' d = (B_SUP a) 'imp' (B_INF d) by Th25;
A7: B_INF d = d by Th25;
consider k4 being Function such that
A8: I_el Y = k4 and
A9: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A10: (O_el Y) 'imp' (I_el Y) = k3 and
A11: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds ((O_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x

proof

let x be Element of Y; :: thesis: ((O_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x
( ((O_el Y) 'imp' (I_el Y)) . x = ('not' ((O_el Y) . x)) 'or' ((I_el Y) . x) & (I_el Y) . x = TRUE ) by Def11, Def14;
hence ((O_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x ; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A10, A8;
then A12: (O_el Y) 'imp' (I_el Y) = I_el Y by A10, A11, A8, A9, FUNCT_1:9;
consider k4 being Function such that
A13: O_el Y = k4 and
A14: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A15: (I_el Y) 'imp' (O_el Y) = k3 and
A16: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x

proof

let x be Element of Y; :: thesis: ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x
(O_el Y) . x = FALSE by Def13;
then A17: ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) = ('not' TRUE) 'or' FALSE by Def14;
((I_el Y) 'imp' (O_el Y)) . x = ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) by Def11;
hence ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x by A17, Def13; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A15, A13;
then A18: (I_el Y) 'imp' (O_el Y) = O_el Y by A15, A16, A13, A14, FUNCT_1:9;
consider k4 being Function such that
A19: I_el Y = k4 and
A20: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A21: (O_el Y) 'imp' (O_el Y) = k3 and
A22: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds ((O_el Y) 'imp' (O_el Y)) . x = (I_el Y) . x

proof

let x be Element of Y; :: thesis: ((O_el Y) 'imp' (O_el Y)) . x = (I_el Y) . x
(O_el Y) . x = FALSE by Def13;
then ((O_el Y) 'imp' (O_el Y)) . x = TRUE 'or' FALSE by Def11;
hence ((O_el Y) 'imp' (O_el Y)) . x = (I_el Y) . x by Def14; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A21, A19;
then A23: (O_el Y) 'imp' (O_el Y) = I_el Y by A21, A22, A19, A20, FUNCT_1:9;
A24: d 'imp' (B_INF a) = (B_INF d) 'imp' (B_INF a) by Th25;
A25: (B_SUP a) 'imp' d = (B_SUP a) 'imp' (B_SUP d) by Th25;

A26: now

assume A27: ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' 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 A27;

case A28: ( ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

A29: now

assume A30: ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' 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 A30;

case A31: ( ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

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

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = TRUE
( d . x = TRUE & a . x = TRUE ) by A28, A31;
then (a 'imp' d) . x = ('not' TRUE) 'or' TRUE by Def11;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

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

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = TRUE
( d . x = TRUE & a . x = TRUE ) by A28, A31;
then (d 'imp' a) . x = ('not' TRUE) 'or' TRUE by Def11;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

B_INF a = I_el Y by A31, Def16;
then A34: d 'imp' (B_INF a) = I_el Y by A24, A5, A28, Def16;
A35: B_SUP a = I_el Y by A31, Def17;
B_SUP d = I_el Y by A28, Def17;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A25, A5, A33, A32, A35, A34, Def16; :: thesis: verum

end;

case A36: ( ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

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

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = FALSE
( (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) & d . x = TRUE ) by A28, Def11;
hence (d 'imp' a) . x = FALSE by A36; :: thesis: verum

end;

A38: now

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

end;

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

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = TRUE
( d . x = TRUE & a . x = FALSE ) by A28, A36;
then (a 'imp' d) . x = ('not' FALSE) 'or' TRUE by Def11;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

A41: B_SUP a = O_el Y by A36, Def17;
B_SUP d = I_el Y by A28, Def17;
then A42: (B_SUP a) 'imp' d = I_el Y by A12, A41, Th25;
A43: B_INF a = O_el Y by A36, Def16;
B_INF d = I_el Y by A28, Def16;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A18, A38, A40, A43, A42, Def16; :: thesis: verum

end;

case A44: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

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

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = TRUE
( (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) & a . x = TRUE ) by A44, Def11;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A46: B_INF d = I_el Y by A28, Def16;
A47: for x being Element of Y holds (a 'imp' d) . x = TRUE

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = TRUE
( (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) & d . x = TRUE ) by A28, Def11;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

( B_INF a = I_el Y & B_SUP a = O_el Y ) by A44, Def16, Def17;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A6, A5, A12, A45, A47, A46, Def16; :: thesis: verum

end;

end;

end;

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

end;

now

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

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = TRUE
('not' (a . x)) 'or' (d . x) = (('not' a) . x) 'or' (d . x) by MARGREL1:def 20;
then ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' d) . x by Def7;
then ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' (I_el Y)) . x by A7, A28, Def16;
then A49: ('not' (a . x)) 'or' (d . x) = (I_el Y) . x by Th13;
(a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def11;
hence (a 'imp' d) . x = TRUE by A49, Def14; :: thesis: verum

end;

A50: B_INF d = I_el Y by A28, Def16;
assume that
A51: not for x being Element of Y holds a . x = TRUE and
A52: not for x being Element of Y holds a . x = FALSE ; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A53: B_INF a = O_el Y by A51, Def16;
B_SUP a = I_el Y by A52, Def17;
then A54: (B_SUP a) 'imp' d = I_el Y by A5, A50, Th25;
consider k4 being Function such that
A55: a = k4 and
A56: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A57: d 'imp' a = k3 and
A58: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds (d 'imp' a) . x = a . x

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = a . x
('not' (d . x)) 'or' (a . x) = (('not' d) . x) 'or' (a . x) by MARGREL1:def 20;
then ('not' (d . x)) 'or' (a . x) = (('not' d) 'or' a) . x by Def7;
then ('not' (d . x)) 'or' (a . x) = (('not' (I_el Y)) 'or' a) . x by A7, A28, Def16;
then A59: ('not' (d . x)) 'or' (a . x) = ((O_el Y) 'or' a) . x by Th5;
(d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def11;
hence (d 'imp' a) . x = a . x by A59, Th12; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A57, A55;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A18, A50, A53, A57, A58, A55, A56, A48, A54, Def16, FUNCT_1:9; :: thesis: verum

end;

hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A29; :: thesis: verum

end;

case A60: ( ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

A61: now

assume A62: ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' 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 A62;

case A63: ( ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

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

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = FALSE
( d . x = FALSE & a . x = TRUE ) by A60, A63;
then (a 'imp' d) . x = ('not' TRUE) 'or' FALSE by Def11;
hence (a 'imp' d) . x = FALSE ; :: thesis: verum

end;

A65: now

assume A66: for x being Element of Y holds (a 'imp' d) . x = TRUE ; :: thesis: for x being Element of Y holds contradiction
let x be Element of Y; :: thesis: contradiction
(a 'imp' d) . x = TRUE by A66;
hence contradiction by A64; :: thesis: verum

end;

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

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = TRUE
( d . x = FALSE & a . x = TRUE ) by A60, A63;
then (d 'imp' a) . x = ('not' FALSE) 'or' TRUE by Def11;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A68: B_SUP a = I_el Y by A63, Def17;
B_SUP d = O_el Y by A60, Def17;
then A69: (B_SUP a) 'imp' d = O_el Y by A18, A68, Th25;
A70: B_INF a = I_el Y by A63, Def16;
B_INF d = O_el Y by A60, Def16;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A12, A67, A65, A70, A69, Def16; :: thesis: verum

end;

case A71: ( ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

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

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = TRUE
( d . x = FALSE & a . x = FALSE ) by A60, A71;
then (d 'imp' a) . x = ('not' FALSE) 'or' FALSE by Def11;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A73: B_INF d = O_el Y by A60, Def16;
A74: for x being Element of Y holds (a 'imp' d) . x = TRUE

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = TRUE
( (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) & a . x = FALSE ) by A71, Def11;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

( B_INF a = O_el Y & B_SUP a = O_el Y ) by A71, Def16, Def17;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A6, A23, A72, A74, A73, Def16; :: thesis: verum

end;

case A75: ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) ) ; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

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

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = TRUE
( (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) & a . x = FALSE ) by A75, Def11;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

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

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = TRUE
( (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) & a . x = TRUE ) by A75, Def11;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A78: B_INF d = O_el Y by A60, Def16;
B_SUP a = O_el Y by A75, Def17;
then A79: (B_SUP a) 'imp' d = I_el Y by A23, A78, Th25;
B_INF a = I_el Y by A75, Def16;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A12, A77, A76, A78, A79, Def16; :: thesis: verum

end;

end;

end;

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

end;

now

A80: B_INF d = O_el Y by A60, Def16;
A81: for x being Element of Y holds (d 'imp' a) . x = TRUE

proof

let x be Element of Y; :: thesis: (d 'imp' a) . x = TRUE
('not' (d . x)) 'or' (a . x) = (('not' d) . x) 'or' (a . x) by MARGREL1:def 20;
then ('not' (d . x)) 'or' (a . x) = (('not' (O_el Y)) 'or' a) . x by A7, A80, Def7;
then ('not' (d . x)) 'or' (a . x) = ((I_el Y) 'or' a) . x by Th5;
then ('not' (d . x)) 'or' (a . x) = (I_el Y) . x by Th13;
then ('not' (d . x)) 'or' (a . x) = TRUE by Def14;
hence (d 'imp' a) . x = TRUE by Def11; :: thesis: verum

end;

consider k4 being Function such that
A82: 'not' a = k4 and
A83: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
consider k3 being Function such that
A84: a 'imp' d = k3 and
A85: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
for x being Element of Y holds (a 'imp' d) . x = ('not' a) . x

proof

let x be Element of Y; :: thesis: (a 'imp' d) . x = ('not' a) . x
('not' (a . x)) 'or' (d . x) = (('not' a) . x) 'or' (d . x) by MARGREL1:def 20;
then ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' d) . x by Def7;
then ('not' (a . x)) 'or' (d . x) = ('not' a) . x by A7, A80, Th12;
hence (a 'imp' d) . x = ('not' a) . x by Def11; :: thesis: verum

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A84, A82;
then a 'imp' d = 'not' a by A84, A85, A82, A83, FUNCT_1:9;
then A86: B_INF (a 'imp' d) = 'not' (B_SUP a) by Th22;
assume ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
then A87: ( B_INF a = O_el Y & B_SUP a = I_el Y ) by Def16, Def17;
B_INF d = O_el Y by A60, Def16;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A24, A6, A18, A23, A81, A86, A87, Def16, Th5; :: thesis: verum

end;

hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A61; :: thesis: verum

end;

case A88: ( ( 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

let x be Element of Y; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
d . x = FALSE by A88;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A88; :: thesis: verum

end;

end;

end;

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

end;

now

assume that
A89: not for x being Element of Y holds d . x = TRUE and
A90: not for x being Element of Y holds d . x = FALSE ; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

now

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

case d = O_el Y ; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A90, Def13; :: thesis: verum

end;

case d = I_el Y ; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A89, Def14; :: thesis: verum

end;

end;

end;

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

end;

hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A26; :: thesis: verum