take
f
=
id
S
;
:: thesis:
f
is
isomorphic
f
"
=
id
S
by
TOPGRP_1:2
;
hence
f
is
isomorphic
;
:: thesis:
verum