let R be Relation; :: thesis: for a being set st R is Order of {a} holds
R = id {a}
let a be set ; :: thesis: ( R is Order of {a} implies R = id {a} )
assume A1: R is Order of {a} ; :: thesis: R = id {a}
then A2: R <> {} ;
R c= [:{a},{a}:] by A1;
then R c= {[a,a]} by ZFMISC_1:29;
then R = {[a,a]} by A2, ZFMISC_1:33;
hence R = id {a} by SYSREL:13; :: thesis: verum