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

consider k3 being Function such that
A6: ( (I_el Y) 'imp' (I_el Y) = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A7: ( I_el Y = 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 A5, A6, A7;
then A8: (I_el Y) 'imp' (I_el Y) = I_el Y by A6, A7, FUNCT_1:9;
A9: 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
A10: ((O_el Y) 'imp' (I_el Y)) . x = ('not' ((O_el Y) . x)) 'or' ((I_el Y) . x) by Def11;
(I_el Y) . x = TRUE by Def14;
hence ((O_el Y) 'imp' (I_el Y)) . x = (I_el Y) . x by A10; :: thesis: verum

end;

consider k3 being Function such that
A11: ( (O_el Y) 'imp' (I_el Y) = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A12: ( I_el Y = 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 A9, A11, A12;
then A13: (O_el Y) 'imp' (I_el Y) = I_el Y by A11, A12, FUNCT_1:9;
A14: 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
A15: ((I_el Y) 'imp' (O_el Y)) . x = ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) by Def11;
(O_el Y) . x = FALSE by Def13;
then ('not' ((I_el Y) . x)) 'or' ((O_el Y) . x) = ('not' TRUE ) 'or' FALSE by Def14;
hence ((I_el Y) 'imp' (O_el Y)) . x = (O_el Y) . x by A15, Def13; :: thesis: verum

end;

consider k3 being Function such that
A16: ( (I_el Y) 'imp' (O_el Y) = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A17: ( O_el Y = 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 A14, A16, A17;
then A18: (I_el Y) 'imp' (O_el Y) = O_el Y by A16, A17, FUNCT_1:9;
A19: 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;

consider k3 being Function such that
A20: ( (O_el Y) 'imp' (O_el Y) = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A21: ( I_el Y = 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 A19, A20, A21;
then A22: (O_el Y) 'imp' (O_el Y) = I_el Y by A20, A21, FUNCT_1:9;

A23: now

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

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

A26: now

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

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

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
A30: d . x = TRUE by A25;
a . x = TRUE by A28;
then (d 'imp' a) . x = ('not' TRUE ) 'or' TRUE by A30, Def11;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

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
A32: d . x = TRUE by A25;
a . x = TRUE by A28;
then (a 'imp' d) . x = ('not' TRUE ) 'or' TRUE by A32, Def11;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

A33: B_SUP d = I_el Y by A25, Def17;
A34: B_INF a = I_el Y by A28, Def16;
A35: B_SUP a = I_el Y by A28, Def17;
d 'imp' (B_INF a) = I_el Y by A2, A8, A25, A34, Def16;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A3, A8, A29, A31, A33, A35, 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
A38: (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def11;
d . x = TRUE by A25;
hence (d 'imp' a) . x = FALSE by A36, A38; :: thesis: verum

end;

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

proof

now

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

end;

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

end;

A41: 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
A42: d . x = TRUE by A25;
a . x = FALSE by A36;
then (a 'imp' d) . x = ('not' FALSE ) 'or' TRUE by A42, Def11;
hence (a 'imp' d) . x = TRUE ; :: thesis: verum

end;

A43: B_INF d = I_el Y by A25, Def16;
A44: B_SUP d = I_el Y by A25, Def17;
A45: B_INF a = O_el Y by A36, Def16;
B_SUP a = O_el Y by A36, Def17;
then (B_SUP a) 'imp' d = I_el Y by A13, A44, Th25;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A2, A18, A39, A41, A43, A45, Def16; :: thesis: verum

end;

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

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
A48: (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def11;
a . x = TRUE by A46;
hence (d 'imp' a) . x = TRUE by A48; :: thesis: verum

end;

A49: 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
A50: (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def11;
d . x = TRUE by A25;
hence (a 'imp' d) . x = TRUE by A50; :: thesis: verum

end;

A51: B_INF d = I_el Y by A25, Def16;
A52: B_INF a = I_el Y by A46, Def16;
B_SUP a = O_el Y by A46, Def17;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A2, A4, A8, A13, A47, A49, A51, A52, 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

assume A53: ( 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 )
A54: B_INF d = I_el Y by A25, Def16;
A55: B_INF a = O_el Y by A53, Def16;
A56: B_SUP a = I_el Y by A53, Def17;
A57: 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
A58: (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def11;
('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 A1, A25, Def16;
then ('not' (d . x)) 'or' (a . x) = ((O_el Y) 'or' a) . x by Th5;
hence (d 'imp' a) . x = a . x by A58, Th12; :: thesis: verum

end;

consider k3 being Function such that
A59: ( d 'imp' a = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A60: ( a = k4 & dom k4 = Y & rng k4 c= BOOLEAN ) by FUNCT_2:def 2;
A61: for u being set st u in Y holds
k3 . u = k4 . u by A57, A59, A60;
A62: 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
A63: (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def11;
('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 A1, A25, Def16;
then ('not' (a . x)) 'or' (d . x) = (I_el Y) . x by Th13;
hence (a 'imp' d) . x = TRUE by A63, Def14; :: thesis: verum

end;

(B_SUP a) 'imp' d = I_el Y by A8, A54, A56, Th25;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A2, A18, A54, A55, A59, A60, A61, A62, 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 A26; :: thesis: verum

end;

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

A65: now

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

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

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

end;

A70: 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
A71: d . x = FALSE by A64;
a . x = TRUE by A67;
then (a 'imp' d) . x = ('not' TRUE ) 'or' FALSE by A71, Def11;
hence (a 'imp' d) . x = FALSE ; :: thesis: verum

end;

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

proof

now

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

end;

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

end;

A74: B_INF d = O_el Y by A64, Def16;
A75: B_SUP d = O_el Y by A64, Def17;
A76: B_INF a = I_el Y by A67, Def16;
B_SUP a = I_el Y by A67, Def17;
then (B_SUP a) 'imp' d = O_el Y by A18, A75, Th25;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A2, A13, A68, A72, A74, A76, Def16; :: thesis: verum

end;

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

A78: 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
A79: d . x = FALSE by A64;
a . x = FALSE by A77;
then (d 'imp' a) . x = ('not' FALSE ) 'or' FALSE by A79, Def11;
hence (d 'imp' a) . x = TRUE ; :: thesis: verum

end;

A80: 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
A81: (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def11;
a . x = FALSE by A77;
hence (a 'imp' d) . x = TRUE by A81; :: thesis: verum

end;

A82: B_INF d = O_el Y by A64, Def16;
A83: B_INF a = O_el Y by A77, Def16;
B_SUP a = O_el Y by A77, Def17;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A2, A4, A22, A78, A80, A82, A83, Def16; :: thesis: verum

end;

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

A85: 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
A86: (d 'imp' a) . x = ('not' (d . x)) 'or' (a . x) by Def11;
a . x = TRUE by A84;
hence (d 'imp' a) . x = TRUE by A86; :: thesis: verum

end;

A87: 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
A88: (a 'imp' d) . x = ('not' (a . x)) 'or' (d . x) by Def11;
a . x = FALSE by A84;
hence (a 'imp' d) . x = TRUE by A88; :: thesis: verum

end;

A89: B_INF d = O_el Y by A64, Def16;
A90: B_INF a = I_el Y by A84, Def16;
B_SUP a = O_el Y by A84, Def17;
then (B_SUP a) 'imp' d = I_el Y by A22, A89, Th25;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A2, A13, A85, A87, A89, A90, 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

assume A91: ( 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 )
A92: B_INF d = O_el Y by A64, Def16;
A93: 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 A1, A92, 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;

A94: 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 A1, A92, Th12;
hence (a 'imp' d) . x = ('not' a) . x by Def11; :: thesis: verum

end;

consider k3 being Function such that
A95: ( a 'imp' d = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A96: ( 'not' 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 A94, A95, A96;
then a 'imp' d = 'not' a by A95, A96, FUNCT_1:9;
then A97: B_INF (a 'imp' d) = 'not' (B_SUP a) by Th22;
A98: B_INF d = O_el Y by A64, Def16;
A99: B_INF a = O_el Y by A91, Def16;
B_SUP a = I_el Y by A91, Def17;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A2, A4, A18, A22, A93, A97, A98, A99, 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 A65; :: thesis: verum

end;

case A100: ( ( 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 A100;
hence ( B_INF (d 'imp' a) = d 'imp' (B_INF a) & B_INF (a 'imp' d) = (B_SUP a) 'imp' d ) by A100; :: 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 A101: ( 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 '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 A101, 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 A101, 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 A23; :: thesis: verum