let Y be non empty set ; :: thesis: for a being Element of Funcs Y,BOOLEAN
for PA being a_partition of Y holds 'not' (B_INF a,PA) = B_SUP ('not' a),PA
let a be Element of Funcs Y,BOOLEAN ; :: thesis: for PA being a_partition of Y holds 'not' (B_INF a,PA) = B_SUP ('not' a),PA
let PA be a_partition of Y; :: thesis: 'not' (B_INF a,PA) = B_SUP ('not' a),PA
A1: for y being Element of Y holds ('not' (B_INF a,PA)) . y = (B_SUP ('not' a),PA) . y

proof

let y be Element of Y; :: thesis: ('not' (B_INF a,PA)) . y = (B_SUP ('not' a),PA) . y

A2: now

assume A3: ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) & ex x being Element of Y st
( x in EqClass y,PA & ('not' a) . x = TRUE ) ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A4: ( x1 in EqClass y,PA & ('not' a) . x1 = TRUE ) ;
('not' ('not' a)) . x1 = 'not' TRUE by A4, MARGREL1:def 20;
hence contradiction by A3, A4; :: thesis: verum

end;

A5: now

assume A6: ( ( for x being Element of Y st x in EqClass y,PA holds
a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass y,PA or not ('not' a) . x = TRUE ) ) ) ; :: thesis: ('not' (B_INF a,PA)) . y = (B_SUP ('not' a),PA) . y
then (B_INF a,PA) . y = TRUE by Def19;
then ('not' (B_INF a,PA)) . y = 'not' TRUE by MARGREL1:def 20;
hence ('not' (B_INF a,PA)) . y = (B_SUP ('not' a),PA) . y by A6, Def20; :: thesis: verum

end;

A7: now

assume A8: ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) & ex x being Element of Y st
( x in EqClass y,PA & ('not' a) . x = TRUE ) ) ; :: thesis: ('not' (B_INF a,PA)) . y = (B_SUP ('not' a),PA) . y
then (B_INF a,PA) . y = FALSE by Def19;
then ('not' (B_INF a,PA)) . y = 'not' FALSE by MARGREL1:def 20;
hence ('not' (B_INF a,PA)) . y = (B_SUP ('not' a),PA) . y by A8, Def20; :: thesis: verum

end;

now

assume A9: ( ex x being Element of Y st
( x in EqClass y,PA & not a . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass y,PA or not ('not' a) . x = TRUE ) ) ) ; :: thesis: contradiction
then consider x1 being Element of Y such that
A10: ( x1 in EqClass y,PA & a . x1 <> TRUE ) ;
a . x1 = FALSE by A10, XBOOLEAN:def 3;
then ('not' a) . x1 = 'not' FALSE by MARGREL1:def 20;
hence contradiction by A9, A10; :: thesis: verum

end;

hence ('not' (B_INF a,PA)) . y = (B_SUP ('not' a),PA) . y by A2, A5, A7; :: thesis: verum

end;

consider k3 being Function such that
A11: ( 'not' (B_INF a,PA) = k3 & dom k3 = Y & rng k3 c= BOOLEAN ) by FUNCT_2:def 2;
consider k4 being Function such that
A12: ( B_SUP ('not' a),PA = 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 A1, A11, A12;
hence 'not' (B_INF a,PA) = B_SUP ('not' a),PA by A11, A12, FUNCT_1:9; :: thesis: verum