let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
let a be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
let G be Subset of (PARTITIONS Y); :: thesis: for A, B being a_partition of Y holds All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
let A, B be a_partition of Y; :: thesis: All ((All (('not' a),A,G)),B,G) '<' 'not' (All ((All (a,B,G)),A,G))
let z be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (All ((All (('not' a),A,G)),B,G)) . z = TRUE or ('not' (All ((All (a,B,G)),A,G))) . z = TRUE )
A1: z in EqClass (z,(CompF (A,G))) by EQREL_1:def 6;
A2: z in EqClass (z,(CompF (B,G))) by EQREL_1:def 6;
assume A3: (All ((All (('not' a),A,G)),B,G)) . z = TRUE ; :: thesis: ('not' (All ((All (a,B,G)),A,G))) . z = TRUE

now :: thesis: for x being Element of Y st x in EqClass (z,(CompF (B,G))) holds
(All (('not' a),A,G)) . x = TRUE

assume ex x being Element of Y st
( x in EqClass (z,(CompF (B,G))) & not (All (('not' a),A,G)) . x = TRUE ) ; :: thesis: contradiction
then (B_INF ((All (('not' a),A,G)),(CompF (B,G)))) . z = FALSE by BVFUNC_1:def 16;
hence contradiction by A3, BVFUNC_2:def 9; :: thesis: verum

end;

then ( All (('not' a),A,G) = B_INF (('not' a),(CompF (A,G))) & (All (('not' a),A,G)) . z = TRUE ) by A2, BVFUNC_2:def 9;
then ('not' a) . z = TRUE by A1, BVFUNC_1:def 16;
then 'not' (a . z) = TRUE by MARGREL1:def 19;
then (B_INF (a,(CompF (B,G)))) . z = FALSE by A2, BVFUNC_1:def 16;
then (All (a,B,G)) . z = FALSE by BVFUNC_2:def 9;
then (B_INF ((All (a,B,G)),(CompF (A,G)))) . z = FALSE by A1, BVFUNC_1:def 16;
then (All ((All (a,B,G)),A,G)) . z = FALSE by BVFUNC_2:def 9;
then 'not' ((All ((All (a,B,G)),A,G)) . z) = TRUE ;
hence ('not' (All ((All (a,B,G)),A,G))) . z = TRUE by MARGREL1:def 19; :: thesis: verum