let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for d being constant Function of 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 Function of Y,BOOLEAN; :: thesis: for d being constant Function of 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 Function of Y,BOOLEAN; :: thesis: ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )
A5: (I_el Y) 'imp' (I_el Y) = I_el Y

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: ((I_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x
(I_el Y) . x = TRUE by Def11;
then ((I_el Y) 'imp' (I_el Y)) . x = ('not' TRUE) 'or' TRUE by Def8;
hence ((I_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x by Def11; :: thesis: verum

end;

A6: (B_SUP a) 'imp' d = (B_SUP a) 'imp' (B_INF d) by Th22;
A7: B_INF d = d by Th22;
A12: (O_el Y) 'imp' (I_el Y) = I_el Y

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: 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 Def8, Def11;
hence ((O_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x ; :: thesis: verum

end;

A18: (I_el Y) 'imp' (O_el Y) = O_el Y

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x
(O_el Y) . x = FALSE by Def10;
then A17: ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) = ('not' TRUE) 'or' FALSE by Def11;
((I_el Y) 'imp' (O_el Y)) . x = ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) by Def8;
hence ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x by A17, Def10; :: thesis: verum

end;

A23: (O_el Y) 'imp' (O_el Y) = I_el Y

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: ((O_el Y) 'imp' (O_el Y)) . x = (I_el Y) . x
(O_el Y) . x = FALSE by Def10;
then ((O_el Y) 'imp' (O_el Y)) . x = TRUE 'or' FALSE by Def8;
hence ((O_el Y) 'imp' (O_el Y)) . x = (I_el Y) . x by Def11; :: thesis: verum

end;

A24: d 'imp' (B_INF a) = (B_INF d) 'imp' (B_INF a) by Th22;
A25: (B_SUP a) 'imp' d = (B_SUP a) 'imp' (B_SUP d) by Th22;

A26: now :: thesis: ( ( for x being Element of Y holds d . x = TRUE or for x being Element of Y holds d . x = FALSE ) implies ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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 :: thesis: ( ( ( for x being Element of Y holds d . x = TRUE ) & not for x being Element of Y holds d . x = FALSE & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) or ( ( for x being Element of Y holds d . x = FALSE ) & not for x being Element of Y holds d . x = TRUE & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) or ( ( for x being Element of Y holds d . x = TRUE ) & ( for x being Element of Y holds d . x = FALSE ) & ( 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 ) ) ) )

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 :: thesis: ( ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) implies ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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 :: thesis: ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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 Def8;
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 Def8;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

B_INF a = I_el Y by A31, Def13;
then A34: d 'imp' (B_INF a) = I_el Y by A24, A5, A28, Def13;
A35: B_SUP a = I_el Y by A31, Def14;
B_SUP d = I_el Y by A28, Def14;
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, Def13; :: 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, Def8;
hence (d 'imp' a) . x = FALSE by A36; :: thesis: verum

end;

A38: now :: thesis: ( ( for x being Element of Y holds (d 'imp' a) . x = TRUE ) implies for x being Element of Y holds contradiction )

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 Def8;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

A41: B_SUP a = O_el Y by A36, Def14;
B_SUP d = I_el Y by A28, Def14;
then A42: (B_SUP a) 'imp' d = I_el Y by A12, A41, Th22;
A43: B_INF a = O_el Y by A36, Def13;
B_INF d = I_el Y by A28, Def13;
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, Def13; :: 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, Def8;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A46: B_INF d = I_el Y by A28, Def13;
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, Def8;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

( B_INF a = I_el Y & B_SUP a = O_el Y ) by A44, Def13, Def14;
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, Def13; :: 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 :: thesis: ( not for x being Element of Y holds a . x = TRUE & not for x being Element of Y holds a . x = FALSE implies ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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 19;
then ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' d) . x by Def4;
then B49: ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' (I_el Y)) . x by A7, A28, Def13;
(a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def8;
hence (a 'imp' d) . x = TRUE by Th10, Def11, B49; :: thesis: verum

end;

A50: B_INF d = I_el Y by A28, Def13;
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, Def13;
B_SUP a = I_el Y by A52, Def14;
then A54: (B_SUP a) 'imp' d = I_el Y by A5, A50, Th22;
d 'imp' a = a

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (d 'imp' a) . x = a . x
('not' (d . x)) 'or' (a . x) = (('not' d) . x) 'or' (a . x) by MARGREL1:def 19;
then ('not' (d . x)) 'or' (a . x) = (('not' d) 'or' a) . x by Def4;
then ('not' (d . x)) 'or' (a . x) = (('not' (I_el Y)) 'or' a) . x by A7, A28, Def13;
then A59: ('not' (d . x)) 'or' (a . x) = ((O_el Y) 'or' a) . x by Th2;
(d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def8;
hence (d 'imp' a) . x = a . x by A59, Th9; :: 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 A24, A18, A28, Def13, A53, A48, A54; :: 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 :: thesis: ( ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) implies ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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 :: thesis: ( ( ( for x being Element of Y holds a . x = TRUE ) & not for x being Element of Y holds a . x = FALSE & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) or ( ( for x being Element of Y holds a . x = FALSE ) & not for x being Element of Y holds a . x = TRUE & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) or ( ( for x being Element of Y holds a . x = FALSE ) & ( for x being Element of Y holds a . x = TRUE ) & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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 Def8;
hence (a 'imp' d) . x = FALSE ; :: thesis: verum

end;

A65: now :: thesis: ( ( for x being Element of Y holds (a 'imp' d) . x = TRUE ) implies for x being Element of Y holds contradiction )

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 Def8;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A68: B_SUP a = I_el Y by A63, Def14;
B_SUP d = O_el Y by A60, Def14;
then A69: (B_SUP a) 'imp' d = O_el Y by A18, A68, Th22;
A70: B_INF a = I_el Y by A63, Def13;
B_INF d = O_el Y by A60, Def13;
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, Def13; :: 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 Def8;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A73: B_INF d = O_el Y by A60, Def13;
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, Def8;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

( B_INF a = O_el Y & B_SUP a = O_el Y ) by A71, Def13, Def14;
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, Def13; :: 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, Def8;
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, Def8;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A78: B_INF d = O_el Y by A60, Def13;
B_SUP a = O_el Y by A75, Def14;
then A79: (B_SUP a) 'imp' d = I_el Y by A23, A78, Th22;
B_INF a = I_el Y by A75, Def13;
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, Def13; :: 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 :: thesis: ( not for x being Element of Y holds a . x = TRUE & not for x being Element of Y holds a . x = FALSE implies ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

A80: B_INF d = O_el Y by A60, Def13;
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 19;
then ('not' (d . x)) 'or' (a . x) = (('not' (O_el Y)) 'or' a) . x by A7, A80, Def4;
then ('not' (d . x)) 'or' (a . x) = ((I_el Y) 'or' a) . x by Th2;
then ('not' (d . x)) 'or' (a . x) = TRUE by Def11, Th10;
hence (d 'imp' a) . x = TRUE by Def8; :: thesis: verum

end;

a 'imp' d = 'not' a

proof

let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (a 'imp' d) . x = ('not' a) . x
('not' (a . x)) 'or' (d . x) = (('not' a) . x) 'or' (d . x) by MARGREL1:def 19;
then ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' d) . x by Def4;
then ('not' (a . x)) 'or' (d . x) = ('not' a) . x by A7, A80, Th9;
hence (a 'imp' d) . x = ('not' a) . x by Def8; :: thesis: verum

end;

then A86: B_INF (a 'imp' d) = 'not' (B_SUP a) by Th19;
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 Def13, Def14;
B_INF d = O_el Y by A60, Def13;
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, Def13, Th2; :: 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 :: thesis: ( not for x being Element of Y holds d . x = TRUE & not for x being Element of Y holds d . x = FALSE implies ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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 :: thesis: ( ( d = O_el Y & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) or ( d = I_el Y & B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) )

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

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, Def10; :: 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, Def11; :: 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