let Y be non empty set ; 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; 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, 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; BVFUNC_1:def 12 ( 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 17;
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: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;
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 16; verum