begin
theorem set00:
for
X,
Y,
x being
set st not
x in X holds
X \ (Y \/ {x}) = X \ Y
theorem ssf0:
theorem SPpart0:
theorem SPpart:
theorem Sinfset:
begin
:: deftheorem Lclique defines connected DILWORTH:def 1 :
theorem DClique:
theorem
theorem Clique36b:
theorem Clique37:
theorem
theorem ExtClique:
theorem ExtCliquemin:
:: deftheorem LAChain defines stable DILWORTH:def 2 :
theorem
theorem AChain36b:
theorem ACClique:
theorem AChain0:
theorem AChain1:
begin
:: deftheorem Lfheight defines with_finite_clique# DILWORTH:def 3 :
:: deftheorem Lheight defines clique# DILWORTH:def 4 :
theorem
theorem Height4:
:: deftheorem Lfwidth defines with_finite_stability# DILWORTH:def 5 :
:: deftheorem Lwidth defines stability# DILWORTH:def 6 :
theorem Width3:
theorem Width4:
begin
:: deftheorem defines Lower DILWORTH:def 7 :
:: deftheorem defines Upper DILWORTH:def 8 :
theorem ABAC0:
theorem ABunion:
theorem Pminmin:
theorem Pmaxmax:
:: deftheorem Lmin defines minimals DILWORTH:def 9 :
:: deftheorem Lmax defines maximals DILWORTH:def 10 :
theorem PCAamin:
theorem PCAbmax:
begin
theorem SPClique:
theorem SPClique1:
theorem SPAChain1:
theorem SPAChain:
theorem SPmax:
theorem SPmin:
theorem PbeSmax:
theorem PabSmin:
theorem Pmaxmin:
theorem
theorem Pminmax:
theorem
theorem PCAmin:
theorem PCAmax:
theorem Hsubp0:
theorem
theorem Wsubp0:
theorem Wsubp1:
begin
:: deftheorem LCpart defines Clique-wise DILWORTH:def 11 :
theorem Chpw:
theorem ACpart1:
theorem ACpart2:
theorem Main:
:: deftheorem LACpart defines StableSet-wise DILWORTH:def 12 :
theorem
begin
theorem DWf:
:: deftheorem Lsc defines strong-chain DILWORTH:def 13 :
theorem Maxsc:
theorem
theorem
begin
theorem CSR:
theorem