RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (x "/\" N), the InternalRel of (x "/\" N) #) by WAYBEL_2:def 3;
then the InternalRel of (x "/\" N) is_reflexive_in the carrier of (x "/\" N) by ORDERS_2:def 2;
hence x "/\" N is reflexive ; :: thesis: verum