let P1, P2 be IncProjStr ; :: thesis: ( IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) implies for A1 being Subset of the Points of P1
for A2 being Subset of the Points of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2 )
assume A1: IncProjStr(# the Points of P1, the Lines of P1, the Inc of P1 #) = IncProjStr(# the Points of P2, the Lines of P2, the Inc of P2 #) ; :: thesis: for A1 being Subset of the Points of P1
for A2 being Subset of the Points of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let A1 be Subset of the Points of P1; :: thesis: for A2 being Subset of the Points of P2 st A1 = A2 holds
for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let A2 be Subset of the Points of P2; :: thesis: ( A1 = A2 implies for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2 )
assume A2: A1 = A2 ; :: thesis: for L1 being LINE of P1
for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let L1 be LINE of P1; :: thesis: for L2 being LINE of P2 st L1 = L2 & A1 on L1 holds
A2 on L2
let L2 be LINE of P2; :: thesis: ( L1 = L2 & A1 on L1 implies A2 on L2 )
assume that
A3: L1 = L2 and
A4: A1 on L1 ; :: thesis: A2 on L2
thus A2 on L2 :: thesis: verum
proof
let A be POINT of P2; :: according to INCSP_1:def 4 :: thesis: ( not A in A2 or A on L2 )
consider B being POINT of P1 such that
A5: A = B by A1;
assume A in A2 ; :: thesis: A on L2
then B on L1 by A2, A4, A5;
then [A,L2] in the Inc of P2 by A1, A3, A5;
hence A on L2 ; :: thesis: verum
end;