let a, b be object ; :: thesis: ( <*a*> = <*b*> implies a = b )
assume A1: <*a*> = <*b*> ; :: thesis: a = b
thus a = <*a*> . 1
.= b by A1, Def8 ; :: thesis: verum