theorem :: DILWORTH:37

for R being transitive antisymmetric with_finite_clique# RelStr holds Upper (minimals R) = [#] R