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' (All a,PA,G) = Ex ('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' (All a,PA,G) = Ex ('not' a),PA,G
let a be Element of Funcs Y,BOOLEAN ; :: thesis: for PA being a_partition of Y holds 'not' (All a,PA,G) = Ex ('not' a),PA,G
let PA be a_partition of Y; :: thesis: 'not' (All a,PA,G) = Ex ('not' a),PA,G
A1: for z being Element of Y holds ('not' (B_INF a,(CompF PA,G))) . z = (B_SUP ('not' a),(CompF PA,G)) . z

proof

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

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

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

then consider x1 being Element of Y such that
A3: ( x1 in EqClass z,(CompF PA,G) & ('not' a) . x1 = TRUE ) ;
'not' (a . x1) = TRUE by A3, MARGREL1:def 20;
then a . x1 = FALSE by MARGREL1:41;
hence ('not' (B_INF a,(CompF PA,G))) . z = (B_SUP ('not' a),(CompF PA,G)) . z by A2, A3; :: thesis: verum

end;

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

then A5: (B_INF a,(CompF PA,G)) . z = TRUE by BVFUNC_1:def 19;
A6: (B_SUP ('not' a),(CompF PA,G)) . z = FALSE by A4, BVFUNC_1:def 20;
('not' (B_INF a,(CompF PA,G))) . z = 'not' TRUE by A5, MARGREL1:def 20;
hence ('not' (B_INF a,(CompF PA,G))) . z = (B_SUP ('not' a),(CompF PA,G)) . z by A6, MARGREL1:41; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

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