begin
theorem Th1:
for
X,
Y,
x being
set st not
x in X holds
X \ (Y \/ {x}) = X \ Y
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
begin
:: deftheorem Def1 defines connected DILWORTH:def 1 :
for R being RelStr
for S being Subset of R holds
( S is connected iff the InternalRel of R is_connected_in S );
theorem Th6:
theorem
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
:: deftheorem Def2 defines stable DILWORTH:def 2 :
for R being RelStr
for S being Subset of R holds
( S is stable iff for x, y being Element of R st x in S & y in S & x <> y holds
( not x <= y & not y <= x ) );
theorem
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
begin
:: deftheorem Def3 defines with_finite_clique# DILWORTH:def 3 :
for R being RelStr holds
( R is with_finite_clique# iff ex C being finite Clique of R st
for D being finite Clique of R holds card D <= card C );
:: deftheorem Def4 defines clique# DILWORTH:def 4 :
for R being with_finite_clique# RelStr
for b2 being Nat holds
( b2 = clique# R iff ( ex C being finite Clique of R st card C = b2 & ( for T being finite Clique of R holds card T <= b2 ) ) );
theorem
theorem Th19:
:: deftheorem Def5 defines with_finite_stability# DILWORTH:def 5 :
for R being RelStr holds
( R is with_finite_stability# iff ex A being finite StableSet of R st
for B being finite StableSet of R holds card B <= card A );
:: deftheorem Def6 defines stability# DILWORTH:def 6 :
for R being with_finite_stability# RelStr
for b2 being Nat holds
( b2 = stability# R iff ( ex A being finite StableSet of R st card A = b2 & ( for T being finite StableSet of R holds card T <= b2 ) ) );
theorem Th20:
theorem Th21:
begin
:: deftheorem defines Lower DILWORTH:def 7 :
for R being RelStr
for X being Subset of R holds Lower X = X \/ (downarrow X);
:: deftheorem defines Upper DILWORTH:def 8 :
for R being RelStr
for X being Subset of R holds Upper X = X \/ (uparrow X);
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
:: deftheorem Def9 defines minimals DILWORTH:def 9 :
for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = minimals R iff for x being Element of R holds
( x in b2 iff x is_minimal_in [#] R ) ) ) & ( R is empty implies ( b2 = minimals R iff b2 = {} ) ) );
:: deftheorem Def10 defines maximals DILWORTH:def 10 :
for R being RelStr
for b2 being Subset of R holds
( ( not R is empty implies ( b2 = maximals R iff for x being Element of R holds
( x in b2 iff x is_maximal_in [#] R ) ) ) & ( R is empty implies ( b2 = maximals R iff b2 = {} ) ) );
theorem Th26:
theorem Th27:
begin
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem Th33:
theorem Th34:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem Th45:
begin
:: deftheorem Def11 defines Clique-wise DILWORTH:def 11 :
for R being RelStr
for P being a_partition of the carrier of R holds
( P is Clique-wise iff for x being set st x in P holds
x is Clique of R );
theorem Th46:
theorem Th47:
theorem Th48:
theorem Th49:
:: deftheorem Def12 defines StableSet-wise DILWORTH:def 12 :
for R being RelStr
for P being a_partition of the carrier of R holds
( P is StableSet-wise iff for x being set st x in P holds
x is StableSet of R );
theorem
begin
theorem Th51:
:: deftheorem Def13 defines strong-chain DILWORTH:def 13 :
for R being non empty with_finite_stability# RelStr
for C being Subset of R holds
( C is strong-chain iff for S being non empty finite Subset of R ex P being Clique-partition of (subrelstr S) st
( card P <= stability# R & ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) ) );
theorem Th52:
theorem
theorem
begin
theorem Th55:
theorem