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 ) )

.= 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

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

thus All ((All (a,P,G)),Q,G) =
B_INF ((All (a,P,G)),(CompF (Q,G)))
by BVFUNC_2:def 9
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 ) )

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;(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 )

given x being Element of Y such that A11:
x in EqClass (y,(CompF (Q,G)))
and ( 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

end;(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

hence
(B_INF ((B_INF (a,(CompF (Q,G)))),(CompF (P,G)))) . y = TRUE
by BVFUNC_1:def 16; :: thesis: verum
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

end;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

hence
(B_INF (a,(CompF (Q,G)))) . x = TRUE
by BVFUNC_1:def 16; :: thesis: verum
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;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

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

.= 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