RelStr(# the carrier of N,the InternalRel of N #) = RelStr(# the carrier of (f * N),the InternalRel of (f * N) #) by Def8;
hence the InternalRel of (f * N) is_reflexive_in the carrier of (f * N) by ORDERS_2:def 4; :: according to ORDERS_2:def 4 :: thesis: verum