theorem Th55: :: DILWORTH:55

for R being finite transitive antisymmetric RelStr
for r, s being Nat holds
( not card R = (r * s) + 1 or ex C being Clique of R st card C >= r + 1 or ex A being StableSet of R st card A >= s + 1 )