set RO = the InternalRel of O;
A1: field the InternalRel of O c= the carrier of O \/ the carrier of O by RELSET_1:8;
thus ( O is irreflexive implies the InternalRel of O is irreflexive ) :: thesis: ( the InternalRel of O is irreflexive implies O is irreflexive )
proof
assume A2: O is irreflexive ; :: thesis: the InternalRel of O is irreflexive
let x be object ; :: according to RELAT_2:def 2,RELAT_2:def 10 :: thesis: ( not x in field the InternalRel of O or not [x,x] in the InternalRel of O )
thus ( not x in field the InternalRel of O or not [x,x] in the InternalRel of O ) by A1, A2; :: thesis: verum
end;
assume A3: the InternalRel of O is_irreflexive_in field the InternalRel of O ; :: according to RELAT_2:def 10 :: thesis: O is irreflexive
let x be set ; :: according to NECKLACE:def 5 :: thesis: ( not x in the carrier of O or not [x,x] in the InternalRel of O )
assume x in the carrier of O ; :: thesis: not [x,x] in the InternalRel of O
per cases ( x in field the InternalRel of O or not x in field the InternalRel of O ) ;
suppose x in field the InternalRel of O ; :: thesis: not [x,x] in the InternalRel of O
hence not [x,x] in the InternalRel of O by A3; :: thesis: verum
end;
suppose not x in field the InternalRel of O ; :: thesis: not [x,x] in the InternalRel of O
hence not [x,x] in the InternalRel of O by RELAT_1:15; :: thesis: verum
end;
end;