let Y be non empty set ; :: thesis: for a being Function of Y,BOOLEAN
for G being Subset of ()
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 ()
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 (); :: 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 ;
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
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 ;
assume z in EqClass (x,(CompF (P,G))) ; :: thesis: (Ex (a,Q,G)) . z = TRUE
then [z,x] in ERl ('/\' (G \ {P})) by ;
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 ;
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 ;
then reconsider u = u as Element of Y by ORDERS_1:12;
[u,y] in ERl ('/\' (G \ {P})) by ;
then ( All (a,P,G) = B_INF (a,(CompF (P,G))) & u in EqClass (y,(CompF (P,G))) ) by ;
then A13: a . u = TRUE by ;
( Ex (a,Q,G) = B_SUP (a,(CompF (Q,G))) & u in EqClass (z,(CompF (Q,G))) ) by ;
hence (Ex (a,Q,G)) . z = TRUE by ; :: thesis: verum
end;
All ((Ex (a,Q,G)),P,G) = B_INF ((Ex (a,Q,G)),(CompF (P,G))) by BVFUNC_2:def 9;
hence (All ((Ex (a,Q,G)),P,G)) . x = TRUE by ; :: thesis: verum