begin
begin
begin
Lm1:
for Y being non empty set
for G being Subset of (PARTITIONS Y) st G is independent holds
for P, Q being Subset of (PARTITIONS Y) st P c= G & Q c= G holds
(ERl ('/\' P)) * (ERl ('/\' Q)) c= (ERl ('/\' Q)) * (ERl ('/\' P))
theorem Th15:
for
Y being 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
All (
(All (a,P,G)),
Q,
G)
= All (
(All (a,Q,G)),
P,
G)
theorem
for
Y being 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 (
(Ex (a,P,G)),
Q,
G)
= Ex (
(Ex (a,Q,G)),
P,
G)
theorem
for
Y being 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)
begin