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)} )

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

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

assume A3:
for o being Object of C holds <^o,o^> = {(idm o)}
; :: thesis: 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)}

end;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^> ) )

hence
<^o,o^> = {(idm o)}
by TARSKI:def 1; :: thesis: verum( ( 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^> ) )

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

thus
( j = idm o implies j in <^o,o^> )
by Th13; :: thesis: verum
( 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;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

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