reconsider y = x, z = f . x as Point of by PRE_TOPC:55;
x <> f . x by A1, ABIAN:def 4;
then reconsider a = HC z,y,o,r as Point of by Th6;
take a ; :: thesis: ex y, z being Point of st
( y = x & z = f . x & a = HC z,y,o,r )
thus ex y, z being Point of st
( y = x & z = f . x & a = HC z,y,o,r ) ; :: thesis: verum