let R be non empty Poset; :: thesis: for s1, s2 being Element of R st s1 <= s2 holds
CComp s1 = CComp s2
let s1, s2 be Element of R; :: thesis: ( s1 <= s2 implies CComp s1 = CComp s2 )
assume s1 <= s2 ; :: thesis: CComp s1 = CComp s2
then [s1,s2] in Path_Rel R by Th2;
hence CComp s1 = CComp s2 by EQREL_1:35; :: thesis: verum