set XX = the Points of IPP;
defpred S₁[ set , set ] 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 ) );
A2: for x, y being set st x in the Points of IPP & S₁[x,y] holds
y in the Points of IPP ;
A3: for x, y1, y2 being set st x in the Points of IPP & S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let x, y1, y2 be set ; :: 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 y1 = y1, y2 = y2 as POINT of IPP by A5, A6;
reconsider x = x as POINT of IPP by A4;
consider A1 being Element of the Lines of IPP such that
A7: ( p on A1 & x on A1 & y1 on A1 ) by A5;
( p on A1 & x on A1 & y2 on A1 ) by A1, A6, A7, INCPROJ:def 9;
hence y1 = y2 by A1, A5, A6, A7, INCPROJ:def 9; :: thesis: verum

end;

consider f being PartFunc of the Points of IPP,the Points of IPP such that
A8: for x being set holds
( x in dom f iff ( x in the Points of IPP & ex y being set st S₁[x,y] ) ) and
A9: for x being set st x in dom f holds
S₁[x,f . x] from PARTFUN1:sch 2(A2, 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 A10: 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 )
A11: ( x in dom f implies x on K )

proof

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

end;

( x on K implies x in dom f )

proof

assume A12: x on K ; :: thesis: x in dom f
consider X being LINE of IPP such that
A13: ( p on X & x on X ) by INCPROJ:def 10;
ex y being POINT of IPP st
( y on L & y on X ) by INCPROJ:def 14;
hence x in dom f by A8, A12, A13; :: thesis: verum

end;

hence ( x in dom f iff x on K ) by A11; :: 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 A14: ( x on K & y on L ) ; :: thesis: ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) )
thus ( f . x = y iff ex X being LINE of IPP st
( p on X & x on X & y on X ) ) :: thesis: verum

proof

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

proof

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

end;

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

proof

assume A17: ex X being LINE of IPP st
( p on X & x on X & y on X ) ; :: thesis: f . x = y
x in dom f by A10, A14;
then S₁[x,f . x] by A9;
hence f . x = y by A3, A14, A17; :: 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 A15; :: thesis: verum

end;