let S1, S2 be IncProjStr ; :: thesis: for F1, F2 being IncProjMap of S1,S2 st IncProjMap(# the point-map of F1,the line-map of F1 #) = IncProjMap(# the point-map of F2,the line-map of F2 #) & F1 is incidence_preserving holds
F2 is incidence_preserving
let F1, F2 be IncProjMap of S1,S2; :: thesis: ( IncProjMap(# the point-map of F1,the line-map of F1 #) = IncProjMap(# the point-map of F2,the line-map of F2 #) & F1 is incidence_preserving implies F2 is incidence_preserving )
assume A1: ( IncProjMap(# the point-map of F1,the line-map of F1 #) = IncProjMap(# the point-map of F2,the line-map of F2 #) & F1 is incidence_preserving ) ; :: thesis: F2 is incidence_preserving
let A1 be POINT of S1; :: according to COMBGRAS:def 8 :: thesis: for L1 being LINE of S1 holds
( A1 on L1 iff F2 . A1 on F2 . L1 )
let L1 be LINE of S1; :: thesis: ( A1 on L1 iff F2 . A1 on F2 . L1 )
( F2 . A1 = F1 . A1 & F2 . L1 = F1 . L1 ) by A1;
hence ( A1 on L1 iff F2 . A1 on F2 . L1 ) by A1, Def8; :: thesis: verum