defpred S_{1}[ object , object ] means ex x being LINE of (IncProjSp_of real_projective_plane) st

( $1 = x & $2 = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } );

A1: for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds

ex y being object st

( y in the Lines of (IncProjSp_of real_projective_plane) & S_{1}[x,y] )

A13: for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A1);

for x being LINE of (IncProjSp_of real_projective_plane) holds f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }_{1} being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) st

for x being LINE of (IncProjSp_of real_projective_plane) holds b_{1} . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }
; :: thesis: verum

( $1 = x & $2 = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } );

A1: for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds

ex y being object st

( y in the Lines of (IncProjSp_of real_projective_plane) & S

proof

consider f being Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) such that
let x be object ; :: thesis: ( x in the Lines of (IncProjSp_of real_projective_plane) implies ex y being object st

( y in the Lines of (IncProjSp_of real_projective_plane) & S_{1}[x,y] ) )

assume x in the Lines of (IncProjSp_of real_projective_plane) ; :: thesis: ex y being object st

( y in the Lines of (IncProjSp_of real_projective_plane) & S_{1}[x,y] )

then reconsider x9 = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;

set y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } ;

consider p, q being Point of real_projective_plane such that

A2: p <> q and

A3: x9 = Line (p,q) by COLLSP:def 7, INCPROJ:4;

reconsider p9 = (homography N) . p, q9 = (homography N) . q as Point of real_projective_plane by FUNCT_2:5;

A4: { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } = Line (p9,q9)

reconsider y = y9 as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;

y is Element of the Lines of (IncProjSp_of real_projective_plane) ;

then reconsider y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } as Element of the Lines of (IncProjSp_of real_projective_plane) by A4;

take y ; :: thesis: ( y in the Lines of (IncProjSp_of real_projective_plane) & S_{1}[x,y] )

thus ( y in the Lines of (IncProjSp_of real_projective_plane) & S_{1}[x,y] )
; :: thesis: verum

end;( y in the Lines of (IncProjSp_of real_projective_plane) & S

assume x in the Lines of (IncProjSp_of real_projective_plane) ; :: thesis: ex y being object st

( y in the Lines of (IncProjSp_of real_projective_plane) & S

then reconsider x9 = x as Element of the Lines of (IncProjSp_of real_projective_plane) ;

set y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } ;

consider p, q being Point of real_projective_plane such that

A2: p <> q and

A3: x9 = Line (p,q) by COLLSP:def 7, INCPROJ:4;

reconsider p9 = (homography N) . p, q9 = (homography N) . q as Point of real_projective_plane by FUNCT_2:5;

A4: { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } = Line (p9,q9)

proof

reconsider y9 = Line (p9,q9) as LINE of real_projective_plane by A2, ANPROJ_9:16, COLLSP:def 7;
A5:
{ ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } c= Line (p9,q9)

end;proof

Line (p9,q9) c= { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 }
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } or x in Line (p9,q9) )

assume x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } ; :: thesis: x in Line (p9,q9)

then consider Px being POINT of (IncProjSp_of real_projective_plane) such that

A6: x = (homography N) . 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 A7, INCPROJ:5;

reconsider p1 = p, q1 = q, r1 = Px, p2 = p9, q2 = q9 as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography N) . p1,(homography N) . q1,(homography N) . r1 are_collinear by A8, A3, COLLSP:11, ANPROJ_8:102;

hence x in Line (p9,q9) by A6, COLLSP:11; :: thesis: verum

end;assume x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } ; :: thesis: x in Line (p9,q9)

then consider Px being POINT of (IncProjSp_of real_projective_plane) such that

A6: x = (homography N) . 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 A7, INCPROJ:5;

reconsider p1 = p, q1 = q, r1 = Px, p2 = p9, q2 = q9 as Point of (ProjectiveSpace (TOP-REAL 3)) ;

(homography N) . p1,(homography N) . q1,(homography N) . r1 are_collinear by A8, A3, COLLSP:11, ANPROJ_8:102;

hence x in Line (p9,q9) by A6, COLLSP:11; :: thesis: verum

proof

hence
{ ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } = Line (p9,q9)
by A5; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Line (p9,q9) or x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } )

assume x in Line (p9,q9) ; :: thesis: x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : 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 (ProjectiveSpace (TOP-REAL 3)) ;

reconsider r2 = (homography (N ~)) . r1 as Point of (ProjectiveSpace (TOP-REAL 3)) ;

reconsider r3 = r2 as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;

A11: r1 = (homography N) . r2 by ANPROJ_9:15;

A12: x9 is LINE of real_projective_plane by INCPROJ:4;

r2 in x9 by A3, A10, A11, ANPROJ_8:102, COLLSP:11;

then r3 on x9 by A12, INCPROJ:5;

hence x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } by A11, A9; :: thesis: verum

end;assume x in Line (p9,q9) ; :: thesis: x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : 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 (ProjectiveSpace (TOP-REAL 3)) ;

reconsider r2 = (homography (N ~)) . r1 as Point of (ProjectiveSpace (TOP-REAL 3)) ;

reconsider r3 = r2 as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;

A11: r1 = (homography N) . r2 by ANPROJ_9:15;

A12: x9 is LINE of real_projective_plane by INCPROJ:4;

r2 in x9 by A3, A10, A11, ANPROJ_8:102, COLLSP:11;

then r3 on x9 by A12, INCPROJ:5;

hence x in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } by A11, A9; :: thesis: verum

reconsider y = y9 as LINE of (IncProjSp_of real_projective_plane) by INCPROJ:4;

y is Element of the Lines of (IncProjSp_of real_projective_plane) ;

then reconsider y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x9 } as Element of the Lines of (IncProjSp_of real_projective_plane) by A4;

take y ; :: thesis: ( y in the Lines of (IncProjSp_of real_projective_plane) & S

thus ( y in the Lines of (IncProjSp_of real_projective_plane) & S

A13: for x being object st x in the Lines of (IncProjSp_of real_projective_plane) holds

S

for x being LINE of (IncProjSp_of real_projective_plane) holds f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }

proof

hence
ex b
let x be LINE of (IncProjSp_of real_projective_plane); :: thesis: f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x }

S_{1}[x,f . x]
by A13;

hence f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ; :: thesis: verum

end;S

hence f . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ; :: thesis: verum

for x being LINE of (IncProjSp_of real_projective_plane) holds b