defpred S1[ object , object ] means for p being Point of () st p = \$1 holds
\$2 = tricord2 (p1,p2,p3,p);
set X = the carrier of ();
set Y = the carrier of R^1;
A1: for x being object st x in the carrier of () holds
ex y being object st
( y in the carrier of R^1 & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of () implies ex y being object st
( y in the carrier of R^1 & S1[x,y] ) )

assume x in the carrier of () ; :: thesis: ex y being object st
( y in the carrier of R^1 & S1[x,y] )

then reconsider p0 = x as Point of () ;
reconsider t = tricord2 (p1,p2,p3,p0) as Element of REAL by XREAL_0:def 1;
S1[x,t] ;
hence
ex y being object st
( y in the carrier of R^1 & S1[x,y] ) by TOPMETR:17; :: thesis: verum
end;
ex f being Function of the carrier of (), the carrier of R^1 st
for x being object st x in the carrier of () holds
S1[x,f . x] from then consider g being Function of the carrier of (), the carrier of R^1 such that
A2: for x being object st x in the carrier of () holds
for p being Point of () st p = x holds
g . x = tricord2 (p1,p2,p3,p) ;
reconsider f0 = g as Function of (),R^1 ;
for p being Point of () holds f0 . p = tricord2 (p1,p2,p3,p) by A2;
hence ex b1 being Function of (),R^1 st
for p being Point of () holds b1 . p = tricord2 (p1,p2,p3,p) ; :: thesis: verum