for R being non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is antisymmetric & the InternalRel of R is transitive holds
( R is reflexive & R is antisymmetric & R is transitive )