set R1 = ComplRelStr R;

for x being set st x in the carrier of (ComplRelStr R) holds

not [x,x] in the InternalRel of (ComplRelStr R)

for x being set st x in the carrier of (ComplRelStr R) holds

not [x,x] in the InternalRel of (ComplRelStr R)

proof

hence
ComplRelStr R is irreflexive
; :: thesis: verum
let x be set ; :: thesis: ( x in the carrier of (ComplRelStr R) implies not [x,x] in the InternalRel of (ComplRelStr R) )

assume x in the carrier of (ComplRelStr R) ; :: thesis: not [x,x] in the InternalRel of (ComplRelStr R)

then A1: x in the carrier of R by NECKLACE:def 8;

not [x,x] in the InternalRel of (ComplRelStr R)

end;assume x in the carrier of (ComplRelStr R) ; :: thesis: not [x,x] in the InternalRel of (ComplRelStr R)

then A1: x in the carrier of R by NECKLACE:def 8;

not [x,x] in the InternalRel of (ComplRelStr R)

proof

hence
not [x,x] in the InternalRel of (ComplRelStr R)
; :: thesis: verum
assume
[x,x] in the InternalRel of (ComplRelStr R)
; :: thesis: contradiction

then [x,x] in ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def 8;

then not [x,x] in id the carrier of R by XBOOLE_0:def 5;

hence contradiction by A1, RELAT_1:def 10; :: thesis: verum

end;then [x,x] in ( the InternalRel of R `) \ (id the carrier of R) by NECKLACE:def 8;

then not [x,x] in id the carrier of R by XBOOLE_0:def 5;

hence contradiction by A1, RELAT_1:def 10; :: thesis: verum