theorem Th16: :: MODAL_1:21

for Z being finite Tree
for o being Element of Z st o <> Root Z holds
card (Z | o) < card Z