let Y be non empty set ; :: thesis: for a being Element of Funcs (Y,BOOLEAN) holds
( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) )
let a be Element of Funcs (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 20;
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 20;
hence a . x = TRUE ; :: thesis: verum

end;

A5: now

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

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 20; :: thesis: verum

end;

B_INF a = I_el Y by A7, Def16;
then A9: 'not' (B_INF a) = O_el Y by Th5;
( B_INF ('not' a) = O_el Y & 'not' (B_SUP a) = 'not' (I_el Y) ) by A1, A7, Def16, Def17;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A9, A8, Def17, Th5; :: 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 20; :: thesis: verum

end;

'not' (B_SUP a) = 'not' (O_el Y) by A10, Def17;
then A12: 'not' (B_SUP a) = I_el Y by Th5;
( B_SUP ('not' a) = I_el Y & 'not' (B_INF a) = 'not' (O_el Y) ) by A3, A10, Def16, Def17;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A12, A11, Def16, Th5; :: 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

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, Def16;
then A16: 'not' (B_INF a) = I_el Y by Th5;
( 'not' (B_SUP a) = 'not' (I_el Y) & B_INF ('not' a) = O_el Y ) by A1, A15, Def16, Def17;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A3, A14, A16, Def17, Th5; :: thesis: verum

end;

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