:: deftheorem Def1 defines diagonal ROUGHS_1:def 1 :
for A being RelStr holds
( A is diagonal iff the InternalRel of A c= id the carrier of A );