let R be RelStr ; :: thesis: id the carrier of R misses the InternalRel of (ComplRelStr R)
assume not id the carrier of R misses the InternalRel of (ComplRelStr R) ; :: thesis: contradiction
then (id the carrier of R) /\ the InternalRel of (ComplRelStr R) <> {} ;
then consider a being object such that
A1: a in (id the carrier of R) /\ the InternalRel of (ComplRelStr R) by XBOOLE_0:def 1;
a in the InternalRel of (ComplRelStr R) by A1, XBOOLE_0:def 4;
then A2: a in ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def 8;
a in id the carrier of R by A1, XBOOLE_0:def 4;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum