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

Ex ((All (a,P,G)),Q,G) '<' All ((Ex (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

Ex ((All (a,P,G)),Q,G) '<' All ((Ex (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

Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)

let P, Q be a_partition of Y; :: thesis: ( G is independent implies Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) )

assume A1: G is independent ; :: thesis: Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)

set A = G \ {P};

set B = G \ {Q};

( G \ {P} c= G & G \ {Q} c= G ) by XBOOLE_1:36;

then A2: (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A1, Th14;

A3: CompF (P,G) = '/\' (G \ {P}) by BVFUNC_2:def 7;

A4: Ex ((All (a,P,G)),Q,G) = B_SUP ((All (a,P,G)),(CompF (Q,G))) by BVFUNC_2:def 10;

A5: CompF (Q,G) = '/\' (G \ {Q}) by BVFUNC_2:def 7;

let x be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (Ex ((All (a,P,G)),Q,G)) . x = TRUE or (All ((Ex (a,Q,G)),P,G)) . x = TRUE )

assume A6: (Ex ((All (a,P,G)),Q,G)) . x = TRUE ; :: thesis: (All ((Ex (a,Q,G)),P,G)) . x = TRUE

A7: for z being Element of Y st z in EqClass (x,(CompF (P,G))) holds

(Ex (a,Q,G)) . z = TRUE

hence (All ((Ex (a,Q,G)),P,G)) . x = TRUE by A7, BVFUNC_1:def 16; :: thesis: verum

for G being Subset of (PARTITIONS Y)

for P, Q being a_partition of Y st G is independent holds

Ex ((All (a,P,G)),Q,G) '<' All ((Ex (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

Ex ((All (a,P,G)),Q,G) '<' All ((Ex (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

Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)

let P, Q be a_partition of Y; :: thesis: ( G is independent implies Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G) )

assume A1: G is independent ; :: thesis: Ex ((All (a,P,G)),Q,G) '<' All ((Ex (a,Q,G)),P,G)

set A = G \ {P};

set B = G \ {Q};

( G \ {P} c= G & G \ {Q} c= G ) by XBOOLE_1:36;

then A2: (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) = (ERl ('/\' (G \ {Q}))) * (ERl ('/\' (G \ {P}))) by A1, Th14;

A3: CompF (P,G) = '/\' (G \ {P}) by BVFUNC_2:def 7;

A4: Ex ((All (a,P,G)),Q,G) = B_SUP ((All (a,P,G)),(CompF (Q,G))) by BVFUNC_2:def 10;

A5: CompF (Q,G) = '/\' (G \ {Q}) by BVFUNC_2:def 7;

let x be Element of Y; :: according to BVFUNC_1:def 12 :: thesis: ( not (Ex ((All (a,P,G)),Q,G)) . x = TRUE or (All ((Ex (a,Q,G)),P,G)) . x = TRUE )

assume A6: (Ex ((All (a,P,G)),Q,G)) . x = TRUE ; :: thesis: (All ((Ex (a,Q,G)),P,G)) . x = TRUE

A7: for z being Element of Y st z in EqClass (x,(CompF (P,G))) holds

(Ex (a,Q,G)) . z = TRUE

proof

All ((Ex (a,Q,G)),P,G) = B_INF ((Ex (a,Q,G)),(CompF (P,G)))
by BVFUNC_2:def 9;
let z be Element of Y; :: thesis: ( z in EqClass (x,(CompF (P,G))) implies (Ex (a,Q,G)) . z = TRUE )

consider y being Element of Y such that

A8: y in EqClass (x,(CompF (Q,G))) and

A9: (All (a,P,G)) . y = TRUE by A6, A4, BVFUNC_1:def 17;

assume z in EqClass (x,(CompF (P,G))) ; :: thesis: (Ex (a,Q,G)) . z = TRUE

then [z,x] in ERl ('/\' (G \ {P})) by A3, Th5;

then A10: [x,z] in ERl ('/\' (G \ {P})) by EQREL_1:6;

[y,x] in ERl ('/\' (G \ {Q})) by A5, A8, Th5;

then [y,z] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) by A2, A10, RELAT_1:def 8;

then consider u being object such that

A11: [y,u] in ERl ('/\' (G \ {P})) and

A12: [u,z] in ERl ('/\' (G \ {Q})) by RELAT_1:def 8;

u in field (ERl ('/\' (G \ {Q}))) by A12, RELAT_1:15;

then reconsider u = u as Element of Y by ORDERS_1:12;

[u,y] in ERl ('/\' (G \ {P})) by A11, EQREL_1:6;

then ( All (a,P,G) = B_INF (a,(CompF (P,G))) & u in EqClass (y,(CompF (P,G))) ) by A3, Th5, BVFUNC_2:def 9;

then A13: a . u = TRUE by A9, BVFUNC_1:def 16;

( Ex (a,Q,G) = B_SUP (a,(CompF (Q,G))) & u in EqClass (z,(CompF (Q,G))) ) by A5, A12, Th5, BVFUNC_2:def 10;

hence (Ex (a,Q,G)) . z = TRUE by A13, BVFUNC_1:def 17; :: thesis: verum

end;consider y being Element of Y such that

A8: y in EqClass (x,(CompF (Q,G))) and

A9: (All (a,P,G)) . y = TRUE by A6, A4, BVFUNC_1:def 17;

assume z in EqClass (x,(CompF (P,G))) ; :: thesis: (Ex (a,Q,G)) . z = TRUE

then [z,x] in ERl ('/\' (G \ {P})) by A3, Th5;

then A10: [x,z] in ERl ('/\' (G \ {P})) by EQREL_1:6;

[y,x] in ERl ('/\' (G \ {Q})) by A5, A8, Th5;

then [y,z] in (ERl ('/\' (G \ {P}))) * (ERl ('/\' (G \ {Q}))) by A2, A10, RELAT_1:def 8;

then consider u being object such that

A11: [y,u] in ERl ('/\' (G \ {P})) and

A12: [u,z] in ERl ('/\' (G \ {Q})) by RELAT_1:def 8;

u in field (ERl ('/\' (G \ {Q}))) by A12, RELAT_1:15;

then reconsider u = u as Element of Y by ORDERS_1:12;

[u,y] in ERl ('/\' (G \ {P})) by A11, EQREL_1:6;

then ( All (a,P,G) = B_INF (a,(CompF (P,G))) & u in EqClass (y,(CompF (P,G))) ) by A3, Th5, BVFUNC_2:def 9;

then A13: a . u = TRUE by A9, BVFUNC_1:def 16;

( Ex (a,Q,G) = B_SUP (a,(CompF (Q,G))) & u in EqClass (z,(CompF (Q,G))) ) by A5, A12, Th5, BVFUNC_2:def 10;

hence (Ex (a,Q,G)) . z = TRUE by A13, BVFUNC_1:def 17; :: thesis: verum

hence (All ((Ex (a,Q,G)),P,G)) . x = TRUE by A7, BVFUNC_1:def 16; :: thesis: verum