theorem Th4: :: DILWORTH:4

for X, Y being set
for F being a_partition of Y st Y c< X holds
F \/ {(X \ Y)} is a_partition of X