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 a . x = TRUE ) iff for x being Element of Y holds ('not' a) . x = FALSE )

proof

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

proof

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

end;

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

hence ( ( for x being Element of Y holds a . x = TRUE ) iff for x being Element of Y holds ('not' a) . x = FALSE ) by A2; :: thesis: verum

end;

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

proof

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

proof

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

end;

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

proof

assume A8: 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 A8;
then 'not' (a . x) = TRUE by MARGREL1:def 20;
hence a . x = FALSE ; :: thesis: verum

end;

hence ( ( for x being Element of Y holds a . x = FALSE ) iff for x being Element of Y holds ('not' a) . x = TRUE ) by A6; :: thesis: verum

end;

A9: now

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

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

then B_INF a = I_el Y by Def16;
then A12: 'not' (B_INF a) = O_el Y by Th5;
A13: 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 A11;
hence ('not' a) . x = FALSE by MARGREL1:def 20; :: thesis: verum

end;

A14: B_INF ('not' a) = O_el Y by A5, A11, Def16;
'not' (B_SUP a) = 'not' (I_el Y) by A11, Def17;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A12, A13, A14, Def17, Th5; :: thesis: verum

end;

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

then 'not' (B_SUP a) = 'not' (O_el Y) by Def17;
then A16: 'not' (B_SUP a) = I_el Y by Th5;
A17: 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 A15;
hence ('not' a) . x = TRUE by MARGREL1:def 20; :: thesis: verum

end;

A18: B_SUP ('not' a) = I_el Y by A1, A15, Def17;
'not' (B_INF a) = 'not' (O_el Y) by A15, Def16;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A16, A17, A18, Def16, Th5; :: thesis: verum

end;

case A19: ( ( 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 A19;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A19; :: 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 A20: ( not 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) )
then 'not' (B_INF a) = 'not' (O_el Y) by Def16;
then A21: 'not' (B_INF a) = I_el Y by Th5;
A22: 'not' (B_SUP a) = 'not' (I_el Y) by A20, Def17;
B_INF ('not' a) = O_el Y by A5, A20, Def16;
hence ( 'not' (B_INF a) = B_SUP ('not' a) & 'not' (B_SUP a) = B_INF ('not' a) ) by A1, A20, A21, A22, Def17, Th5; :: thesis: verum

end;

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