let O be non empty RelStr ; :: thesis: ( O is irreflexive implies O is SubIrreFlexive )
set RO = the InternalRel of O;
assume O is irreflexive ; :: thesis: O is SubIrreFlexive
then the InternalRel of O is_irreflexive_in the carrier of O by Def12;
then the InternalRel of O is irreflexive by Th17;
hence O is SubIrreFlexive by Def11; :: thesis: verum