let A be RelStr ; :: thesis: ( A is reflexive & A is trivial implies A is discrete )
assume A1: ( A is reflexive & A is trivial ) ; :: thesis: A is discrete

per cases ( the carrier of A is empty or ex x being set st the carrier of A = {x} ) by A1, REALSET1:def 4;

suppose A3: the carrier of A is empty ; :: thesis: A is discrete

then the InternalRel of A = {} ;
hence A is discrete by A3, ORDERS_3:def 1, RELAT_1:81; :: thesis: verum

end;

suppose ex x being set st the carrier of A = {x} ; :: thesis: A is discrete

then consider x being set such that
A4: the carrier of A = {x} ;
the InternalRel of A c= [:{x},{x}:] by A4;
then the InternalRel of A c= {[x,x]} by ZFMISC_1:35;
then A5: ( the InternalRel of A = {[x,x]} or the InternalRel of A = {} ) by ZFMISC_1:39;
A6: the InternalRel of A is_reflexive_in the carrier of A by A1, ORDERS_2:def 4;
x in the carrier of A by A4, TARSKI:def 1;
then the InternalRel of A = id {x} by A5, A6, RELAT_2:def 1, SYSREL:30;
hence A is discrete by A4, ORDERS_3:def 1; :: thesis: verum

end;

end;