defpred S₁[ 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 & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be object ; :: thesis: ( x in the Points of IPP & S₁[x,y1] & S₁[x,y2] implies y1 = y2 )
assume that
A4: x in the Points of IPP and
A5: S₁[x,y1] and
A6: S₁[x,y2] ; :: thesis: 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; :: thesis: verum

end;

A10: for x, y being object st x in the Points of IPP & S₁[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 S₁[x,y] ) ) and
A12: for x being object st x in dom f holds
S₁[x,f . x] from PARTFUN1:sch 2(A10, A3);
take f ; :: thesis: ( 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 ; :: thesis: ( ( 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 ) :: thesis: 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 ) )

proof

let x be POINT of IPP; :: thesis: ( x in dom f iff x on K )
A14: ( x on K implies x in dom f )

proof

consider X being LINE of IPP such that
A15: ( p on X & x on X ) by INCPROJ:def 5;
assume A16: x on K ; :: thesis: x in dom f
ex y being POINT of IPP st
( y on L & y on X ) by INCPROJ:def 9;
hence x in dom f by A11, A16, A15; :: thesis: verum

end;

( x in dom f implies x on K )

proof

assume x in dom f ; :: thesis: x on K
then S₁[x,f . x] by A12;
hence x on K ; :: thesis: verum

end;

hence ( x in dom f iff x on K ) by A14; :: thesis: verum

end;

let x, y be POINT of IPP; :: thesis: ( 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 ; :: thesis: ( 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 ) )

proof

x in dom f by A13, A17;
then A20: S₁[x,f . x] by A12;
assume f . x = y ; :: thesis: ex X being LINE of IPP st
( p on X & x on X & y on X )
hence ex X being LINE of IPP st
( p on X & x on X & y on X ) by A20; :: thesis: verum

end;

( ex X being LINE of IPP st
( p on X & x on X & y on X ) implies f . x = y )

proof

x in dom f by A13, A17;
then A21: S₁[x,f . x] by A12;
assume ex X being LINE of IPP st
( p on X & x on X & y on X ) ; :: thesis: f . x = y
hence f . x = y by A3, A18, A21; :: thesis: verum

end;

hence ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) by A19; :: thesis: verum