defpred S1[ object , object ] means ex x, y being POINT of IPP st
( x = $1 & y = $2 & x on K & y on L & ex X being LINE of IPP st
( p on X & x on X & y on X ) );
set XX = the Points of IPP;
A3:
for x, y1, y2 being object st x in the Points of IPP & S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( x in the Points of IPP & S1[x,y1] & S1[x,y2] implies y1 = y2 )
assume that A4:
x in the
Points of
IPP
and A5:
S1[
x,
y1]
and A6:
S1[
x,
y2]
;
y1 = y2
reconsider x =
x as
POINT of
IPP by A4;
reconsider y1 =
y1,
y2 =
y2 as
POINT of
IPP by A5, A6;
consider A1 being
Element of the
Lines of
IPP such that A7:
p on A1
and A8:
x on A1
and A9:
y1 on A1
by A5;
y2 on A1
by A1, A6, A7, A8, INCPROJ:def 4;
hence
y1 = y2
by A2, A5, A6, A7, A9, INCPROJ:def 4;
verum
end;
A10:
for x, y being object st x in the Points of IPP & S1[x,y] holds
y in the Points of IPP
;
consider f being PartFunc of the Points of IPP, the Points of IPP such that
A11:
for x being object holds
( x in dom f iff ( x in the Points of IPP & ex y being object st S1[x,y] ) )
and
A12:
for x being object st x in dom f holds
S1[x,f . x]
from PARTFUN1:sch 2(A10, A3);
take
f
; ( dom f c= the Points of IPP & ( for x being POINT of IPP holds
( x in dom f iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) )
thus
dom f c= the Points of IPP
; ( ( for x being POINT of IPP holds
( x in dom f iff x on K ) ) & ( for x, y being POINT of IPP st x on K & y on L holds
( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) ) )
thus A13:
for x being POINT of IPP holds
( x in dom f iff x on K )
for x, y being POINT of IPP st x on K & y on L holds
( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) )
let x, y be POINT of IPP; ( x on K & y on L implies ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) )
assume that
A17:
x on K
and
A18:
y on L
; ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) )
A19:
( f . x = y implies ex X being LINE of IPP st
( p on X & x on X & y on X ) )
( ex X being LINE of IPP st
( p on X & x on X & y on X ) implies f . x = y )
hence
( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) )
by A19; verum