let T be non empty RelStr ; :: thesis: for a being Element of T st T is reflexive & [#] T = {a} holds
T is discrete
let a be Element of T; :: thesis: ( T is reflexive & [#] T = {a} implies T is discrete )
assume A1: T is reflexive ; :: thesis: ( not [#] T = {a} or T is discrete )
assume A2: [#] T = {a} ; :: thesis: T is discrete
set R = the InternalRel of T;
the InternalRel of T = id {a}

proof

A3: ( the InternalRel of T c= [:{a},{a}:] & id {a} = {[a,a]} ) by A2, SYSREL:30;
hence the InternalRel of T c= id {a} by ZFMISC_1:35; :: according to XBOOLE_0:def 10 :: thesis: id {a} c= the InternalRel of T
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in id {a} or x in the InternalRel of T )
assume x in id {a} ; :: thesis: x in the InternalRel of T
then ( x = [a,a] & a >= a ) by A1, A3, ORDERS_2:24, TARSKI:def 1;
hence x in the InternalRel of T by ORDERS_2:def 9; :: thesis: verum

end;

hence T is discrete by A2, Def1; :: thesis: verum