theorem :: DILWORTH:39

for R being transitive antisymmetric with_finite_clique# RelStr holds Lower (maximals R) = [#] R