:: deftheorem 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 = {} ) ) ) );