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 ('not' (Ex a,A,G)),B,G '<' 'not' (Ex (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 ('not' (Ex a,A,G)),B,G '<' 'not' (Ex (All a,B,G),A,G)
let G be Subset of (PARTITIONS Y); :: thesis: for A, B being a_partition of Y holds All ('not' (Ex a,A,G)),B,G '<' 'not' (Ex (All a,B,G),A,G)
let A, B be a_partition of Y; :: thesis: All ('not' (Ex a,A,G)),B,G '<' 'not' (Ex (All a,B,G),A,G)
let z be Element of Y; :: according to BVFUNC_1:def 15 :: thesis: ( not (All ('not' (Ex a,A,G)),B,G) . z = TRUE or ('not' (Ex (All a,B,G),A,G)) . z = TRUE )
A1: ( All ('not' (Ex a,A,G)),B,G = B_INF ('not' (Ex a,A,G)),(CompF B,G) & z in EqClass z,(CompF B,G) ) by BVFUNC_2:def 9, EQREL_1:def 8;
assume (All ('not' (Ex a,A,G)),B,G) . z = TRUE ; :: thesis: ('not' (Ex (All a,B,G),A,G)) . z = TRUE
then ('not' (Ex a,A,G)) . z = TRUE by A1, BVFUNC_1:def 19;
then A2: ( Ex a,A,G = B_SUP a,(CompF A,G) & 'not' ((Ex a,A,G) . z) = TRUE ) by BVFUNC_2:def 10, MARGREL1:def 20;
A3: All a,B,G = B_INF a,(CompF B,G) by BVFUNC_2:def 9;
for x being Element of Y st x in EqClass z,(CompF A,G) holds
(All a,B,G) . x <> TRUE

proof

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

end;

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