defpred S1[ object , object ] means ex x being LINE of st
( \$1 = x & \$2 = { (() . P) where P is POINT of : P on x } );
A1: for x being object st x in the Lines of holds
ex y being object st
( y in the Lines of & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the Lines of implies ex y being object st
( y in the Lines of & S1[x,y] ) )

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

then reconsider x9 = x as Element of the Lines of ;
set y = { (() . P) where P is POINT of : P on x9 } ;
consider p, q being Point of real_projective_plane such that
A2: p <> q and
A3: x9 = Line (p,q) by ;
reconsider p9 = () . p, q9 = () . q as Point of real_projective_plane by FUNCT_2:5;
A4: { ((homography N) . P) where P is POINT of : P on x9 } = Line (p9,q9)
proof
A5: { ((homography N) . P) where P is POINT of : P on x9 } c= Line (p9,q9)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (() . P) where P is POINT of : P on x9 } or x in Line (p9,q9) )
assume x in { (() . P) where P is POINT of : P on x9 } ; :: thesis: x in Line (p9,q9)
then consider Px being POINT of such that
A6: x = () . Px and
A7: Px on x9 ;
reconsider Px = Px as Point of real_projective_plane by INCPROJ:3;
x9 is LINE of real_projective_plane by INCPROJ:4;
then A8: Px in x9 by ;
reconsider p1 = p, q1 = q, r1 = Px, p2 = p9, q2 = q9 as Point of () ;
(homography N) . p1,() . q1,() . r1 are_collinear by ;
hence x in Line (p9,q9) by ; :: thesis: verum
end;
Line (p9,q9) c= { (() . P) where P is POINT of : P on x9 }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (p9,q9) or x in { (() . P) where P is POINT of : P on x9 } )
assume x in Line (p9,q9) ; :: thesis: x in { (() . P) where P is POINT of : P on x9 }
then x in { p where p is Element of real_projective_plane : p9,q9,p are_collinear } by COLLSP:def 5;
then consider x99 being Element of real_projective_plane such that
A9: x = x99 and
A10: p9,q9,x99 are_collinear ;
reconsider p1 = p, q1 = q, r1 = x99, p2 = p9, q2 = q9 as Point of () ;
reconsider r2 = (homography (N ~)) . r1 as Point of () ;
reconsider r3 = r2 as POINT of by INCPROJ:3;
A11: r1 = () . r2 by ANPROJ_9:15;
A12: x9 is LINE of real_projective_plane by INCPROJ:4;
r2 in x9 by ;
then r3 on x9 by ;
hence x in { (() . P) where P is POINT of : P on x9 } by ; :: thesis: verum
end;
hence { ((homography N) . P) where P is POINT of : P on x9 } = Line (p9,q9) by A5; :: thesis: verum
end;
reconsider y9 = Line (p9,q9) as LINE of real_projective_plane by ;
reconsider y = y9 as LINE of by INCPROJ:4;
y is Element of the Lines of ;
then reconsider y = { (() . P) where P is POINT of : P on x9 } as Element of the Lines of by A4;
take y ; :: thesis: ( y in the Lines of & S1[x,y] )
thus ( y in the Lines of & S1[x,y] ) ; :: thesis: verum
end;
consider f being Function of the Lines of , the Lines of such that
A13: for x being object st x in the Lines of holds
S1[x,f . x] from for x being LINE of holds f . x = { (() . P) where P is POINT of : P on x }
proof
let x be LINE of ; :: thesis: f . x = { (() . P) where P is POINT of : P on x }
S1[x,f . x] by A13;
hence f . x = { (() . P) where P is POINT of : P on x } ; :: thesis: verum
end;
hence ex b1 being Function of the Lines of , the Lines of st
for x being LINE of holds b1 . x = { (() . P) where P is POINT of : P on x } ; :: thesis: verum