:: deftheorem defines CComp OSALG_4:def 6 :
for R being non empty Poset
for s1 being Element of R holds CComp s1 = Class ((Path_Rel R),s1);