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