let AS be AffinSpace; :: thesis: ( IncProjSp_of AS is Fanoian implies AS is Fanoian )
set XX = IncProjSp_of AS;
assume A1: IncProjSp_of AS is Fanoian ; :: thesis: AS is Fanoian
for a, b, c, d being Element of AS st a,b // c,d & a,c // b,d & a,d // b,c holds
a,b // a,c
proof
let a, b, c, d be Element of AS; :: thesis: ( a,b // c,d & a,c // b,d & a,d // b,c implies a,b // a,c )
assume that
A2: a,b // c,d and
A3: a,c // b,d and
A4: a,d // b,c ; :: thesis: a,b // a,c
assume A5: not a,b // a,c ; :: thesis: contradiction
then A6: a <> d by A2, AFF_1:4;
then A7: Line (a,d) is being_line by AFF_1:def 3;
A8: now :: thesis: not b = d
assume b = d ; :: thesis: contradiction
then b,a // b,c by A2, AFF_1:4;
then LIN b,a,c by AFF_1:def 1;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5, AFF_1:def 1; :: thesis: verum
end;
then A9: Line (b,d) is being_line by AFF_1:def 3;
A10: now :: thesis: not c = d
assume c = d ; :: thesis: contradiction
then c,a // c,b by A3, AFF_1:4;
then LIN c,a,b by AFF_1:def 1;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5, AFF_1:def 1; :: thesis: verum
end;
then A11: Line (c,d) is being_line by AFF_1:def 3;
A12: a <> c by A5, AFF_1:3;
then A13: Line (a,c) is being_line by AFF_1:def 3;
A14: a <> b by A5, AFF_1:3;
then A15: Line (a,b) is being_line by AFF_1:def 3;
then reconsider a9 = LDir (Line (a,b)), b9 = LDir (Line (a,c)), c9 = LDir (Line (a,d)) as Element of the Points of (IncProjSp_of AS) by A13, A7, Th20;
A16: b <> c by A5, AFF_1:2;
then A17: Line (b,c) is being_line by AFF_1:def 3;
then reconsider L1 = [(Line (a,b)),1], Q1 = [(Line (c,d)),1], R1 = [(Line (b,d)),1], S1 = [(Line (a,c)),1], A1 = [(Line (a,d)),1], B1 = [(Line (b,c)),1] as Element of the Lines of (IncProjSp_of AS) by A15, A11, A9, A13, A7, Th23;
reconsider p = a, q = d, r = c, s = b as Element of the Points of (IncProjSp_of AS) by Th20;
A18: a9 on L1 by A15, Th30;
c in Line (b,c) by AFF_1:15;
then A19: r on B1 by A17, Th26;
b in Line (b,c) by AFF_1:15;
then A20: s on B1 by A17, Th26;
Line (a,d) // Line (b,c) by A4, A16, A6, AFF_1:37;
then Line (a,d) '||' Line (b,c) by A7, A17, AFF_4:40;
then c9 on B1 by A7, A17, Th28;
then A21: {c9,r,s} on B1 by A19, A20, INCSP_1:2;
A22: d in Line (b,d) by AFF_1:15;
then A23: q on R1 by A9, Th26;
A24: c in Line (a,c) by AFF_1:15;
then A25: r on S1 by A13, Th26;
A26: b9 on S1 by A13, Th30;
A27: a in Line (a,c) by AFF_1:15;
then p on S1 by A13, Th26;
then A28: {b9,p,r} on S1 by A25, A26, INCSP_1:2;
A29: Line (a,c) // Line (b,d) by A3, A12, A8, AFF_1:37;
then Line (a,c) '||' Line (b,d) by A9, A13, AFF_4:40;
then A30: b9 on R1 by A9, A13, Th28;
A31: b in Line (b,d) by AFF_1:15;
then s on R1 by A9, Th26;
then A32: {b9,q,s} on R1 by A23, A30, INCSP_1:2;
A33: now :: thesis: not Line (a,c) = Line (b,d)
assume Line (a,c) = Line (b,d) ; :: thesis: contradiction
then LIN a,c,b by A31, AFF_1:def 2;
then LIN a,b,c by AFF_1:6;
hence contradiction by A5, AFF_1:def 1; :: thesis: verum
end;
A34: now :: thesis: ( not q on S1 & not s on S1 )
assume ( q on S1 or s on S1 ) ; :: thesis: contradiction
then ( d in Line (a,c) or b in Line (a,c) ) by Th26;
hence contradiction by A31, A22, A33, A29, AFF_1:45; :: thesis: verum
end;
A35: now :: thesis: ( not p on R1 & not r on R1 )
assume ( p on R1 or r on R1 ) ; :: thesis: contradiction
then ( a in Line (b,d) or c in Line (b,d) ) by Th26;
hence contradiction by A27, A24, A33, A29, AFF_1:45; :: thesis: verum
end;
A36: a in Line (a,b) by AFF_1:15;
then consider Y being Subset of AS such that
A37: Line (a,b) c= Y and
A38: Line (a,c) c= Y and
A39: Y is being_plane by A27, A15, A13, AFF_4:38;
reconsider C1 = [(PDir Y),2] as Element of the Lines of (IncProjSp_of AS) by A39, Th23;
A40: b9 on C1 by A13, A38, A39, Th31;
A41: Line (a,b) // Line (c,d) by A2, A14, A10, AFF_1:37;
then Line (a,b) '||' Line (c,d) by A15, A11, AFF_4:40;
then A42: a9 on Q1 by A15, A11, Th28;
d in Line (a,d) by AFF_1:15;
then A43: q on A1 by A7, Th26;
a in Line (a,d) by AFF_1:15;
then A44: p on A1 by A7, Th26;
c9 on A1 by A7, Th30;
then A45: {c9,p,q} on A1 by A44, A43, INCSP_1:2;
A46: b in Line (a,b) by AFF_1:15;
then A47: s on L1 by A15, Th26;
a9 on C1 by A15, A37, A39, Th31;
then A48: {a9,b9} on C1 by A40, INCSP_1:1;
A49: d in Line (c,d) by AFF_1:15;
then A50: q on Q1 by A11, Th26;
A51: c in Line (c,d) by AFF_1:15;
then r on Q1 by A11, Th26;
then A52: {a9,q,r} on Q1 by A50, A42, INCSP_1:2;
A53: now :: thesis: not Line (a,b) = Line (c,d)
assume Line (a,b) = Line (c,d) ; :: thesis: contradiction
then LIN a,b,c by A51, AFF_1:def 2;
hence contradiction by A5, AFF_1:def 1; :: thesis: verum
end;
A54: now :: thesis: ( not q on L1 & not r on L1 )
assume ( q on L1 or r on L1 ) ; :: thesis: contradiction
then ( d in Line (a,b) or c in Line (a,b) ) by Th26;
hence contradiction by A51, A49, A53, A41, AFF_1:45; :: thesis: verum
end;
A55: now :: thesis: ( not p on Q1 & not s on Q1 )
assume ( p on Q1 or s on Q1 ) ; :: thesis: contradiction
then ( a in Line (c,d) or b in Line (c,d) ) by Th26;
hence contradiction by A36, A46, A53, A41, AFF_1:45; :: thesis: verum
end;
Line (b,d) = b * (Line (a,c)) by A31, A13, A29, AFF_4:def 3;
then Line (b,d) c= Y by A46, A13, A37, A38, A39, AFF_4:28;
then A56: c9 on C1 by A36, A22, A6, A7, A37, A39, Th31, AFF_4:19;
p on L1 by A36, A15, Th26;
then {a9,p,s} on L1 by A47, A18, INCSP_1:2;
hence contradiction by A1, A56, A54, A34, A55, A35, A52, A32, A28, A45, A21, A48, INCPROJ:def 12; :: thesis: verum
end;
hence AS is Fanoian by PAPDESAF:def 1; :: thesis: verum