set TR = pcs-ToleranceRels C;
let i be object ; :: according to FUNCOP_1:def 11 :: thesis: ( not i in proj1 (pcs-ToleranceRels C) or (pcs-ToleranceRels C) . i is set )
assume i in dom (pcs-ToleranceRels C) ; :: thesis: (pcs-ToleranceRels C) . i is set
then ex P being TolStr st
( P = C . i & (pcs-ToleranceRels C) . i = the ToleranceRel of P ) by Def19;
hence (pcs-ToleranceRels C) . i is set ; :: thesis: verum