take f = id S; :: thesis: f is isomorphic
thus f is isomorphic :: thesis: verum

proof

thus f is bijective ; :: according to PENCIL_2:def 4 :: thesis: ( f is open & f " is bijective & f " is open )
thus f is open ; :: thesis: ( f " is bijective & f " is open )
thus ( f " is bijective & f " is open ) by TOPGRP_1:2; :: thesis: verum

end;