let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for a being Function of 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 Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' (All (a,PA,G)) = Ex (('not' a),PA,G)
let a be Function of 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)
let z be Element of Y; :: according to FUNCT_2:def 8 :: thesis: ('not' (All (a,PA,G))) . z = (Ex (('not' a),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 A1: ( ( 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' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z

then consider x1 being Element of Y such that
A2: x1 in EqClass (z,(CompF (PA,G))) and
A3: ('not' a) . x1 = TRUE ;
'not' (a . x1) = TRUE by A3, MARGREL1:def 19;
hence ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A1, A2, MARGREL1:11; :: 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' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z

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

end;

suppose A6: ( 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' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z

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

end;

suppose A8: ( 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' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z

then consider x1 being Element of Y such that
A9: x1 in EqClass (z,(CompF (PA,G))) and
A10: a . x1 <> TRUE ;
('not' a) . x1 <> TRUE by A8, A9;
then 'not' (a . x1) <> TRUE by MARGREL1:def 19;
hence ('not' (All (a,PA,G))) . z = (Ex (('not' a),PA,G)) . z by A10, MARGREL1:11, XBOOLEAN:def 3; :: thesis: verum

end;

end;