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

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