let A be RelStr ; :: thesis: ( A is discrete implies A is diagonal )
assume A is discrete ; :: thesis: A is diagonal
then the InternalRel of A = id the carrier of A by ORDERS_3:def 1;
hence A is diagonal by Def1; :: thesis: verum