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 A1: s1 <= s2 ; :: thesis: CComp s1 = CComp s2
[s1,s2] in Path_Rel R by A1, Th2;
hence CComp s1 = CComp s2 by EQREL_1:44; :: thesis: verum