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

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

A5: (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 A6: ('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 A6, Def10; :: thesis: verum

end;

A7: (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;

A8: d 'imp' (B_INF a) = (B_INF d) 'imp' (B_INF a) by Th21;
A9: (B_SUP a) 'imp' d = (B_SUP a) 'imp' (B_SUP d) by Th21;

A10: 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 A11: ( 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 A11;

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

A13: 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 A14: ( 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 A14;

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

A16: 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 A12, A15;
then (a 'imp' d) . x = ('not' TRUE) 'or' TRUE by Def8;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

A17: 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 A12, A15;
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 A15, Def13;
then A18: d 'imp' (B_INF a) = I_el Y by A8, A1, A12, Def13;
A19: B_SUP a = I_el Y by A15, Def14;
B_SUP d = I_el Y by A12, Def14;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A9, A1, A17, A16, A19, A18, Def13; :: thesis: verum

end;

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

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

end;

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

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

end;

A24: 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 A12, A20;
then (a 'imp' d) . x = ('not' FALSE) 'or' TRUE by Def8;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

A25: B_SUP a = O_el Y by A20, Def14;
B_SUP d = I_el Y by A12, Def14;
then A26: (B_SUP a) 'imp' d = I_el Y by A4, A25, Th21;
A27: B_INF a = O_el Y by A20, Def13;
B_INF d = I_el Y by A12, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A8, A5, A22, A24, A27, A26, Def13; :: 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 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d )

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

end;

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

end;

( B_INF a = I_el Y & B_SUP a = O_el Y ) by A28, Def13, Def14;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A8, A2, A1, A4, A29, A31, A30, 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 ) )

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
('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 A33: ('not' (a . x)) 'or' (d . x) = (('not' a) 'or' (I_el Y)) . x by A3, A12, Def13;
(a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def8;
hence (a 'imp' d) . x = TRUE by Th9, Def11, A33; :: thesis: verum

end;

A34: B_INF d = I_el Y by A12, Def13;
assume that
A35: not for x being Element of Y holds a . x = TRUE and
A36: 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 )
A37: B_INF a = O_el Y by A35, Def13;
B_SUP a = I_el Y by A36, Def14;
then A38: (B_SUP a) 'imp' d = I_el Y by A1, A34, Th21;
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 A3, A12, Def13;
then A39: ('not' (d . x)) 'or' (a . x) = ((O_el Y) 'or' a) . x by Th1;
(d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def8;
hence (d 'imp' a) . x = a . x by A39, Th8; :: 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 A8, A5, A12, Def13, A37, A32, A38; :: 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 A13; :: thesis: verum

end;

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

A41: 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 A42: ( 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 A42;

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

A44: 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 A40, A43;
then (a 'imp' d) . x = ('not' TRUE) 'or' FALSE by Def8;
hence (a 'imp' d) . x = FALSE ; :: thesis: verum

end;

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

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

end;

A47: 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 A40, A43;
then (d 'imp' a) . x = ('not' FALSE) 'or' TRUE by Def8;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A48: B_SUP a = I_el Y by A43, Def14;
B_SUP d = O_el Y by A40, Def14;
then A49: (B_SUP a) 'imp' d = O_el Y by A5, A48, Th21;
A50: B_INF a = I_el Y by A43, Def13;
B_INF d = O_el Y by A40, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A8, A4, A47, A45, A50, A49, Def13; :: thesis: verum

end;

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

A52: 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 A40, A51;
then (d 'imp' a) . x = ('not' FALSE) 'or' FALSE by Def8;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

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

end;

( B_INF a = O_el Y & B_SUP a = O_el Y ) by A51, Def13, Def14;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A8, A2, A7, A52, A54, A53, Def13; :: thesis: verum

end;

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

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

end;

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

end;

A58: B_INF d = O_el Y by A40, Def13;
B_SUP a = O_el Y by A55, Def14;
then A59: (B_SUP a) 'imp' d = I_el Y by A7, A58, Th21;
B_INF a = I_el Y by A55, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A8, A4, A57, A56, A58, A59, 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 ) )

A60: B_INF d = O_el Y by A40, Def13;
A61: 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 A3, A60, Def4;
then ('not' (d . x)) 'or' (a . x) = ((I_el Y) 'or' a) . x by Th1;
then ('not' (d . x)) 'or' (a . x) = TRUE by Def11, Th9;
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 A3, A60, Th8;
hence (a 'imp' d) . x = ('not' a) . x by Def8; :: thesis: verum

end;

then A62: B_INF (a 'imp' d) = 'not' (B_SUP a) by Th18;
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 A63: ( B_INF a = O_el Y & B_SUP a = I_el Y ) by Def13, Def14;
B_INF d = O_el Y by A40, Def13;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A8, A2, A5, A7, A61, A62, A63, Def13, Th1; :: 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 A41; :: thesis: verum

end;

case A64: ( ( 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 A64;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A64; :: 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
A65: not for x being Element of Y holds d . x = TRUE and
A66: 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 Th20;

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 A66, 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 A65, 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 A10; :: thesis: verum