begin
theorem Th1:
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem
canceled;
theorem Th7:
:: deftheorem Def1 defines is_a_dependent_set_of PARTIT1:def 1 :
:: deftheorem Def2 defines is_min_depend PARTIT1:def 2 :
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
:: deftheorem Def3 defines PARTITIONS PARTIT1:def 3 :
begin
:: deftheorem defines '/\' PARTIT1:def 4 :
theorem
theorem
theorem Th17:
definition
let Y be non
empty set ;
let PA,
PB be
a_partition of
Y;
func PA '\/' PB -> a_partition of
Y means :
Def5:
for
d being
set holds
(
d in it iff
d is_min_depend PA,
PB );
existence
ex b1 being a_partition of Y st
for d being set holds
( d in b1 iff d is_min_depend PA,PB )
uniqueness
for b1, b2 being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) & ( for d being set holds
( d in b2 iff d is_min_depend PA,PB ) ) holds
b1 = b2
commutativity
for b1, PA, PB being a_partition of Y st ( for d being set holds
( d in b1 iff d is_min_depend PA,PB ) ) holds
for d being set holds
( d in b1 iff d is_min_depend PB,PA )
end;
:: deftheorem Def5 defines '\/' PARTIT1:def 5 :
theorem
canceled;
theorem Th19:
theorem
theorem Th21:
theorem
begin
theorem Th23:
:: deftheorem Def6 defines ERl PARTIT1:def 6 :
:: deftheorem defines Rel PARTIT1:def 7 :
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem
theorem
theorem
theorem Th33:
theorem
:: deftheorem PARTIT1:def 8 :
canceled;
:: deftheorem defines %O PARTIT1:def 9 :
theorem
theorem Th36:
theorem Th37:
theorem Th38:
theorem
theorem
theorem