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

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