set IR = pcs-InternalRels C;
let i be set ; :: according to MSUALG_4:def 1 :: thesis: ( not i in dom (pcs-InternalRels C) or (pcs-InternalRels C) . i is set )
assume A1: i in dom (pcs-InternalRels C) ; :: thesis: (pcs-InternalRels C) . i is set
dom (pcs-InternalRels C) = I by PARTFUN1:def 4;
then ex P being RelStr st
( P = C . i & (pcs-InternalRels C) . i = the InternalRel of P ) by A1, Def5;
hence (pcs-InternalRels C) . i is set ; :: thesis: verum