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