theorem Th7: :: OSALG_4:7

for R being non empty discrete Poset
for C being Component of R ex x being Element of R st C = {x}