set a = the Point of RAS;
take Phi ( the Point of RAS,x) ; :: thesis: for a being Point of RAS holds Phi ( the Point of RAS,x) = Phi (a,x)
thus for a being Point of RAS holds Phi ( the Point of RAS,x) = Phi (a,x) by Th25; :: thesis: verum