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
; 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) )
; verum