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 )
set R = the InternalRel of T;
assume A2: [#] T = {a} ; :: thesis: T is discrete
the InternalRel of T = id {a}

proof

A3: id {a} = {[a,a]} by SYSREL:13;
the InternalRel of T c= [:{a},{a}:] by A2;
hence the InternalRel of T c= id {a} by A3, ZFMISC_1:29; :: according to XBOOLE_0:def 10 :: thesis: id {a} c= the InternalRel of T
let x be object ; :: 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 A4: x = [a,a] by A3, TARSKI:def 1;
a >= a by A1, ORDERS_2:1;
hence x in the InternalRel of T by A4, ORDERS_2:def 5; :: thesis: verum

end;

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