let Y be non empty set ; for a being Element of Funcs 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 Element of Funcs 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 G be 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 P, Q be a_partition of Y; ( G is independent implies Ex (All a,P,G),Q,G '<' All (Ex a,Q,G),P,G )
assume A1:
G is independent
; 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, Th16;
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; BVFUNC_1:def 15 ( 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
; (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;
( 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 20;
assume
z in EqClass x,
(CompF P,G)
;
(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:12;
[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
set 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:30;
then reconsider u =
u as
Element of
Y by ORDERS_1:97;
[u,y] in ERl ('/\' (G \ {P}))
by A11, EQREL_1:12;
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 19;
(
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 20;
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 A7, BVFUNC_1:def 19; verum