:: deftheorem defines reflexive ALTCAT_2:def 6 :
for C being AltGraph holds
( C is reflexive iff for x being set st x in the carrier of C holds
the Arrows of C . (x,x) <> {} );