let l be Element of the Lines of (IncProjSp_of real_projective_plane); :: thesis: (line_homography (1. (F_Real,3))) . l = l
set X = { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ;
A1: { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } c= l

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } or x in l )
assume x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } ; :: thesis: x in l
then consider P being POINT of (IncProjSp_of real_projective_plane) such that
A2: x = (homography (1. (F_Real,3))) . P and
A3: P on l ;
A4: P is Point of real_projective_plane by INCPROJ:2;
then A5: x = P by A2, ANPROJ_9:14;
l is LINE of real_projective_plane by INCPROJ:4;
hence x in l by A4, A3, A5, INCPROJ:5; :: thesis: verum

end;

l c= { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in l or x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } )
assume A6: x in l ; :: thesis: x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l }
A7: l is LINE of real_projective_plane by INCPROJ:4;
l is Subset of real_projective_plane by INCPROJ:4;
then reconsider x9 = x as Point of real_projective_plane by A6;
reconsider l9 = l as LINE of (IncProjSp_of real_projective_plane) ;
reconsider x99 = x9 as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
A8: x99 on l by A7, A6, INCPROJ:5;
(homography (1. (F_Real,3))) . x99 = x99 by ANPROJ_9:14;
hence x in { ((homography (1. (F_Real,3))) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by A8; :: thesis: verum

end;

hence (line_homography (1. (F_Real,3))) . l = l by A1, Def02; :: thesis: verum