theorem Th4: :: OSALG_4:4

for R being non empty Poset
for s1, s2 being Element of R st s1 <= s2 holds
CComp s1 = CComp s2