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

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