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

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