begin
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
scheme
MinSet{
F1()
-> set ,
F2()
-> Relation,
P1[
set ] } :
ex
X being
set st
(
X in F1() &
P1[
X] & ( for
Y being
set st
Y in F1() &
P1[
Y] holds
[X,Y] in F2() ) )
provided
:: deftheorem defines PartUnion PCOMPS_2:def 1 :
:: deftheorem defines DisjointFam PCOMPS_2:def 2 :
:: deftheorem defines PartUnionNat PCOMPS_2:def 3 :
begin
theorem Th6:
theorem
theorem Th8:
theorem
canceled;
theorem
canceled;
theorem
theorem Th12:
theorem