let C be non empty with_units AltCatStr ; :: thesis: ( C is pseudo-discrete iff for o being Object of C holds <^o,o^> = {(idm o)} )

hereby :: thesis: ( ( for o being Object of C holds <^o,o^> = {(idm o)} ) implies C is pseudo-discrete )

assume A1: C is pseudo-discrete ; :: thesis: for o being Object of C holds <^o,o^> = {(idm o)}
let o be Object of C; :: thesis: <^o,o^> = {(idm o)}

now :: thesis: for j being object holds
( ( j in <^o,o^> implies j = idm o ) & ( j = idm o implies j in <^o,o^> ) )

let j be object ; :: thesis: ( ( j in <^o,o^> implies j = idm o ) & ( j = idm o implies j in <^o,o^> ) )

hereby :: thesis: ( j = idm o implies j in <^o,o^> )

( idm o in <^o,o^> & <^o,o^> is trivial ) by A1, Th13;
then consider i being object such that
A2: <^o,o^> = {i} by ZFMISC_1:131;
assume j in <^o,o^> ; :: thesis: j = idm o
then j = i by A2, TARSKI:def 1;
hence j = idm o by A2, TARSKI:def 1; :: thesis: verum

end;

thus ( j = idm o implies j in <^o,o^> ) by Th13; :: thesis: verum

end;

hence <^o,o^> = {(idm o)} by TARSKI:def 1; :: thesis: verum

end;

assume A3: for o being Object of C holds <^o,o^> = {(idm o)} ; :: thesis: C is pseudo-discrete
let o be Object of C; :: according to ALTCAT_1:def 19 :: thesis: <^o,o^> is trivial
<^o,o^> = {(idm o)} by A3;
hence <^o,o^> is trivial ; :: thesis: verum