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 'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (Ex 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 'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (Ex a,B,G),A,G)
let G be Subset of (PARTITIONS Y); :: thesis: for A, B being a_partition of Y holds 'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (Ex a,B,G),A,G)
let A, B be a_partition of Y; :: thesis: 'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (Ex a,B,G),A,G)
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not ('not' (Ex (Ex a,A,G),B,G)) . z = TRUE or ('not' (All (Ex a,B,G),A,G)) . z = TRUE )
assume ('not' (Ex (Ex a,A,G),B,G)) . z = TRUE ; :: thesis: ('not' (All (Ex a,B,G),A,G)) . z = TRUE
then A1: 'not' ((Ex (Ex a,A,G),B,G) . z) = TRUE by MARGREL1:def 20;

A2: now

assume ex x being Element of Y st
( x in EqClass z,(CompF B,G) & (Ex a,A,G) . x = TRUE ) ; :: thesis: contradiction
then (B_SUP (Ex a,A,G),(CompF B,G)) . z = TRUE by BVFUNC_1:def 20;
then (Ex (Ex a,A,G),B,G) . z = TRUE by BVFUNC_2:def 10;
hence contradiction by A1; :: thesis: verum

end;

A3: Ex a,A,G = B_SUP a,(CompF A,G) by BVFUNC_2:def 10;
A4: for x being Element of Y st x in EqClass z,(CompF B,G) holds
for y being Element of Y st y in EqClass x,(CompF A,G) holds
a . y <> TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass z,(CompF B,G) implies for y being Element of Y st y in EqClass x,(CompF A,G) holds
a . y <> TRUE )
assume x in EqClass z,(CompF B,G) ; :: thesis: for y being Element of Y st y in EqClass x,(CompF A,G) holds
a . y <> TRUE
then (Ex a,A,G) . x <> TRUE by A2;
hence for y being Element of Y st y in EqClass x,(CompF A,G) holds
a . y <> TRUE by A3, BVFUNC_1:def 20; :: thesis: verum

end;

for x being Element of Y st x in EqClass z,(CompF B,G) holds
a . x <> TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass z,(CompF B,G) implies a . x <> TRUE )
A5: x in EqClass x,(CompF A,G) by EQREL_1:def 8;
assume x in EqClass z,(CompF B,G) ; :: thesis: a . x <> TRUE
hence a . x <> TRUE by A4, A5; :: thesis: verum

end;

then (B_SUP a,(CompF B,G)) . z = FALSE by BVFUNC_1:def 20;
then ( z in EqClass z,(CompF A,G) & (Ex a,B,G) . z = FALSE ) by BVFUNC_2:def 10, EQREL_1:def 8;
then (B_INF (Ex a,B,G),(CompF A,G)) . z = FALSE by BVFUNC_1:def 19;
then (All (Ex a,B,G),A,G) . z = FALSE by BVFUNC_2:def 9;
then 'not' ((All (Ex a,B,G),A,G) . z) = TRUE ;
hence ('not' (All (Ex a,B,G),A,G)) . z = TRUE by MARGREL1:def 20; :: thesis: verum