reconsider y = x, z = f . x as Point of (TOP-REAL n) by PRE_TOPC:25;
x <> f . x by A1;
then reconsider a = HC (z,y,o,r) as Point of (Tcircle (o,r)) by Th6;
take a ; :: thesis: ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & a = HC (z,y,o,r) )
thus ex y, z being Point of (TOP-REAL n) st
( y = x & z = f . x & a = HC (z,y,o,r) ) ; :: thesis: verum