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 object st the carrier of A = {x} ) by A1, ZFMISC_1:131;

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

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

end;

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

then consider x being object such that
A3: the carrier of A = {x} ;
the InternalRel of A c= [:{x},{x}:] by A3;
then the InternalRel of A c= {[x,x]} by ZFMISC_1:29;
then A4: ( the InternalRel of A = {[x,x]} or the InternalRel of A = {} ) by ZFMISC_1:33;
A5: the InternalRel of A is_reflexive_in the carrier of A by A1, ORDERS_2:def 2;
x in the carrier of A by A3, TARSKI:def 1;
then the InternalRel of A = id {x} by A4, A5, RELAT_2:def 1, SYSREL:13;
hence A is discrete by A3, ORDERS_3:def 1; :: thesis: verum

end;

end;