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

let j be set ; :: 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^> )

assume A2: j in <^o,o^> ; :: thesis: j = idm o
A3: idm o in <^o,o^> by Th23;
<^o,o^> is trivial by A1, Def21;
then consider i being set such that
A4: <^o,o^> = {i} by A3, REALSET1:def 4;
( j = i & idm o = i ) by A2, A4, TARSKI:def 1;
hence j = idm o ; :: thesis: verum

end;

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

end;

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

end;

assume A5: 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 21 :: thesis: <^o,o^> is trivial
<^o,o^> = {(idm o)} by A5;
hence <^o,o^> is trivial ; :: thesis: verum