let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
let G be Subset of (PARTITIONS Y); :: thesis: for a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
let a be Element of Funcs (Y,BOOLEAN); :: thesis: for PA being a_partition of Y holds 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
let PA be a_partition of Y; :: thesis: 'not' (Ex (a,PA,G)) = All (('not' a),PA,G)
consider k3 being Function such that
A1: 'not' (Ex (a,PA,G)) = k3 and
A2: dom k3 = Y and
rng k3 c= BOOLEAN by FUNCT_2:def 2;
consider k4 being Function such that
A3: All (('not' a),PA,G) = k4 and
A4: dom k4 = Y and
rng k4 c= BOOLEAN by FUNCT_2:def 2;
for z being Element of Y holds ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z

proof

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

per cases ( ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) or ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ) ;

suppose A5: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; :: thesis: ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z

then consider x1 being Element of Y such that
A6: x1 in EqClass (z,(CompF (PA,G))) and
A7: a . x1 = TRUE ;
('not' a) . x1 = 'not' TRUE by A7, MARGREL1:def 19;
then ('not' a) . x1 = FALSE by MARGREL1:11;
hence ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z by A5, A6; :: thesis: verum

end;

suppose A8: ( ( for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; :: thesis: ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z

then (B_SUP (a,(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def 17;
then 'not' ((B_SUP (a,(CompF (PA,G)))) . z) = TRUE by MARGREL1:11;
then ('not' (B_SUP (a,(CompF (PA,G))))) . z = TRUE by MARGREL1:def 19;
hence ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z by A8, BVFUNC_1:def 16; :: thesis: verum

end;

suppose A9: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & a . x = TRUE ) ) ; :: thesis: ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z

then (B_SUP (a,(CompF (PA,G)))) . z = TRUE by BVFUNC_1:def 17;
then A10: ('not' (B_SUP (a,(CompF (PA,G))))) . z = 'not' TRUE by MARGREL1:def 19;
(B_INF (('not' a),(CompF (PA,G)))) . z = FALSE by A9, BVFUNC_1:def 16;
hence ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z by A10, MARGREL1:11; :: thesis: verum

end;

suppose A11: ( ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) & not ('not' a) . x = TRUE ) & ( for x being Element of Y holds
( not x in EqClass (z,(CompF (PA,G))) or not a . x = TRUE ) ) ) ; :: thesis: ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z

then consider x1 being Element of Y such that
A12: x1 in EqClass (z,(CompF (PA,G))) and
A13: ('not' a) . x1 <> TRUE ;
('not' a) . x1 = FALSE by A13, XBOOLEAN:def 3;
then 'not' (a . x1) = FALSE by MARGREL1:def 19;
then a . x1 = TRUE by MARGREL1:11;
hence ('not' (B_SUP (a,(CompF (PA,G))))) . z = (B_INF (('not' a),(CompF (PA,G)))) . z by A11, A12; :: thesis: verum

end;

end;

end;

then for u being set st u in Y holds
k3 . u = k4 . u by A1, A3;
hence 'not' (Ex (a,PA,G)) = All (('not' a),PA,G) by A1, A2, A3, A4, FUNCT_1:2; :: thesis: verum