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

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