set IR = pcs-InternalRels C;
let i be object ; :: according to FUNCOP_1:def 11 :: thesis: ( not i in proj1 (pcs-InternalRels C) or (pcs-InternalRels C) . i is set )
assume i in dom (pcs-InternalRels C) ; :: thesis: (pcs-InternalRels C) . i is set
then ex P being RelStr st
( P = C . i & (pcs-InternalRels C) . i = the InternalRel of P ) by Def5;
hence (pcs-InternalRels C) . i is set ; :: thesis: verum