let Y be non empty set ; :: thesis: for a being Element of Funcs 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 Element of Funcs 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 15 :: 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 8;
A2: z in EqClass z,(CompF B,G) by EQREL_1:def 8;
assume A3: (All (All ('not' a),A,G),B,G) . z = TRUE ; :: thesis: ('not' (All (All a,B,G),A,G)) . z = TRUE

now

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 19;
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 19;
then 'not' (a . z) = TRUE by MARGREL1:def 20;
then (B_INF a,(CompF B,G)) . z = FALSE by A2, BVFUNC_1:def 19;
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 19;
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 20; :: thesis: verum