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)
proof
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)
proof
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;
hence not [x,x] in the InternalRel of (ComplRelStr R) ; :: thesis: verum
end;
hence ComplRelStr R is irreflexive ; :: thesis: verum