begin
theorem Th1:
theorem Th2:
theorem
theorem Th4:
theorem Th5:
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
begin
theorem Th11:
theorem
canceled;
theorem Th13:
theorem
canceled;
theorem
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 Th16:
theorem Th17:
for
Y being 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
All (All a,P,G),
Q,
G = All (All a,Q,G),
P,
G
theorem
for
Y being 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 (Ex a,P,G),
Q,
G = Ex (Ex a,Q,G),
P,
G
theorem
for
Y being 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
begin
:: deftheorem defines {} PARTIT_2:def 1 :
for A, B being set holds {} A,B = {} ;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def3 defines involutive PARTIT_2:def 2 :
for f being Function holds
( f is involutive iff for x being set st x in dom f holds
f . (f . x) = x );
:: deftheorem defines involutive PARTIT_2:def 3 :
for X being non empty set
for f being UnOp of X holds
( f is involutive iff for x being Element of X holds f . (f . x) = x );