let S1, S2 be IncProjStr ; :: thesis: for F1, F2 being IncProjMap over 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 over 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 that
A1: IncProjMap(# the point-map of F1, the line-map of F1 #) = IncProjMap(# the point-map of F2, the line-map of F2 #) and
A2: 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 A2; :: thesis: verum