let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
let a be Function of Y,BOOLEAN; :: thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
A1: ( ( for x being Element of Y holds ('not' a) . x = TRUE ) implies for x being Element of Y holds a . x = FALSE )

proof

assume A2: for x being Element of Y holds ('not' a) . x = TRUE ; :: thesis: for x being Element of Y holds a . x = FALSE
let x be Element of Y; :: thesis: a . x = FALSE
('not' a) . x = TRUE by A2;
then 'not' (a . x) = TRUE by MARGREL1:def 19;
hence a . x = FALSE ; :: thesis: verum

end;

A3: ( ( for x being Element of Y holds ('not' a) . x = FALSE ) implies for x being Element of Y holds a . x = TRUE )

proof

assume A4: for x being Element of Y holds ('not' a) . x = FALSE ; :: thesis: for x being Element of Y holds a . x = TRUE
let x be Element of Y; :: thesis: a . x = TRUE
('not' a) . x = FALSE by A4;
then 'not' (a . x) = FALSE by MARGREL1:def 19;
hence a . x = TRUE ; :: thesis: verum

end;

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

assume A6: ( for x being Element of Y holds a . x = TRUE or for x being Element of Y holds a . x = FALSE ) ; :: thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )

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

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 = TRUE ) & ( for x being Element of Y holds a . x = FALSE ) ) ) by A6;

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

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

proof

let x be Element of Y; :: thesis: ('not' a) . x = FALSE
'not' TRUE = FALSE ;
then 'not' (a . x) = FALSE by A7;
hence ('not' a) . x = FALSE by MARGREL1:def 19; :: thesis: verum

end;

B_INF a = I_el Y by A7, Def13;
then A9: 'not' (B_INF a) = O_el Y by Th1;
( B_INF ('not' a) = O_el Y & 'not' (B_SUP a) = 'not' (I_el Y) ) by A1, A7, Def13, Def14;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A9, A8, Def14, Th1; :: thesis: verum

end;

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

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

proof

let x be Element of Y; :: thesis: ('not' a) . x = TRUE
'not' FALSE = TRUE ;
then 'not' (a . x) = TRUE by A10;
hence ('not' a) . x = TRUE by MARGREL1:def 19; :: thesis: verum

end;

'not' (B_SUP a) = 'not' (O_el Y) by A10, Def14;
then A12: 'not' (B_SUP a) = I_el Y by Th1;
( B_SUP ('not' a) = I_el Y & 'not' (B_INF a) = 'not' (O_el Y) ) by A3, A10, Def13, Def14;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A12, A11, Def13, Th1; :: thesis: verum

end;

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

let x be Element of Y; :: thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
a . x = TRUE by A13;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A13; :: thesis: verum

end;

end;

end;

hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) ; :: 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 ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) )

assume that
A14: not for x being Element of Y holds a . x = TRUE and
A15: not for x being Element of Y holds a . x = FALSE ; :: thesis: ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
'not' (B_INF a) = 'not' (O_el Y) by A14, Def13;
then A16: 'not' (B_INF a) = I_el Y by Th1;
( 'not' (B_SUP a) = 'not' (I_el Y) & B_INF ('not' a) = O_el Y ) by A1, A15, Def13, Def14;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A3, A14, A16, Def14, Th1; :: thesis: verum

end;

hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A5; :: thesis: verum