let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let a be Function of Y,BOOLEAN; :: thesis: for G being Subset of (PARTITIONS Y)
for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let G be Subset of (PARTITIONS Y); :: thesis: for P, Q being a_partition of Y st G is independent holds
All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
let P, Q be a_partition of Y; :: thesis: ( G is independent implies All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G) )
set A = G \ {P};
set B = G \ {Q};
A1: CompF (P,G) = '/\' (G \ {P}) by BVFUNC_2:def 7;
A2: ( G \ {P} c= G & G \ {Q} c= G ) by XBOOLE_1:36;
A3: CompF (Q,G) = '/\' (G \ {Q}) by BVFUNC_2:def 7;
assume G is independent ; :: thesis: All ((All (a,P,G)),Q,G) = All ((All (a,Q,G)),P,G)
then A4: (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A2, Th14;
A5: for y being Element of Y holds
( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) )

proof

let y be Element of Y; :: thesis: ( ( ( for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE ) & ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE ) )

hereby :: thesis: ( ex x being Element of Y st
( x in EqClass (y,(CompF (Q,G))) & not (B_INF (a,(CompF (P,G)))) . x = TRUE ) implies (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE )

assume A6: for x being Element of Y st x in EqClass (y,(CompF (Q,G))) holds
(B_INF (a,(CompF (P,G)))) . x = TRUE ; :: thesis: (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE
for x being Element of Y st x in EqClass (y,(CompF (P,G))) holds
(B_INF (a,(CompF (Q,G)))) . x = TRUE

proof

let x be Element of Y; :: thesis: ( x in EqClass (y,(CompF (P,G))) implies (B_INF (a,(CompF (Q,G)))) . x = TRUE )
assume x in EqClass (y,(CompF (P,G))) ; :: thesis: (B_INF (a,(CompF (Q,G)))) . x = TRUE
then A7: [x,y] in ERl ('/\' (G \ {P})) by A1, Th5;
for z being Element of Y st z in EqClass (x,(CompF (Q,G))) holds
a . z = TRUE

proof

let z be Element of Y; :: thesis: ( z in EqClass (x,(CompF (Q,G))) implies a . z = TRUE )
assume z in EqClass (x,(CompF (Q,G))) ; :: thesis: a . z = TRUE
then [z,x] in ERl ('/\' (G \ {Q})) by A3, Th5;
then [z,y] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) by A4, A7, RELAT_1:def 8;
then consider u being object such that
A8: [z,u] in ERl ('/\' (G \ {P})) and
A9: [u,y] in ERl ('/\' (G \ {Q})) by RELAT_1:def 8;
u in field (ERl ('/\' (G \ {Q}))) by A9, RELAT_1:15;
then reconsider u = u as Element of Y by ORDERS_1:12;
u in EqClass (y,(CompF (Q,G))) by A3, A9, Th5;
then A10: (B_INF (a,(CompF (P,G)))) . u <> FALSE by A6;
z in EqClass (u,(CompF (P,G))) by A1, A8, Th5;
hence a . z = TRUE by A10, BVFUNC_1:def 16; :: thesis: verum

end;

hence (B_INF (a,(CompF (Q,G)))) . x = TRUE by BVFUNC_1:def 16; :: thesis: verum

end;

hence (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE by BVFUNC_1:def 16; :: thesis: verum

end;

given x being Element of Y such that A11: x in EqClass (y,(CompF (Q,G))) and
A12: (B_INF (a,(CompF (P,G)))) . x <> TRUE ; :: thesis: (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE
consider z being Element of Y such that
A13: z in EqClass (x,(CompF (P,G))) and
A14: a . z <> TRUE by A12, BVFUNC_1:def 16;
A15: [x,y] in ERl ('/\' (G \ {Q})) by A3, A11, Th5;
[z,x] in ERl ('/\' (G \ {P})) by A1, A13, Th5;
then [z,y] in (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A4, A15, RELAT_1:def 8;
then consider u being object such that
A16: [z,u] in ERl ('/\' (G \ {Q})) and
A17: [u,y] in ERl ('/\' (G \ {P})) by RELAT_1:def 8;
u in field (ERl ('/\' (G \ {Q}))) by A16, RELAT_1:15;
then reconsider u = u as Element of Y by ORDERS_1:12;
z in EqClass (u,(CompF (Q,G))) by A3, A16, Th5;
then A18: (B_INF (a,(CompF (Q,G)))) . u = FALSE by A14, BVFUNC_1:def 16;
u in EqClass (y,(CompF (P,G))) by A1, A17, Th5;
hence (B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = FALSE by A18, BVFUNC_1:def 16; :: thesis: verum

end;

thus All ((All (a,P,G)),Q,G) = B_INF ((All (a,P,G)),(CompF (Q,G))) by BVFUNC_2:def 9
.= B_INF ((B_INF (a,(CompF (P,G)))),(CompF (Q,G))) by BVFUNC_2:def 9
.= B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G))) by A5, BVFUNC_1:def 16
.= B_INF ((All (a,Q,G)),(CompF (P,G))) by BVFUNC_2:def 9
.= All ((All (a,Q,G)),P,G) by BVFUNC_2:def 9 ; :: thesis: verum