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