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) <> {} by XBOOLE_0:def 7;
then consider a being set 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 9;
then ( a in the InternalRel of R ` & not a in id the carrier 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 5;
then not a in the InternalRel of R by XBOOLE_0:def 5;
hence contradiction by A1, XBOOLE_0:def 4; :: thesis: verum