let AS be AffinSpace; :: thesis: ( IncProjSp_of AS is Fanoian implies AS is Fanoian )
assume A1: IncProjSp_of AS is Fanoian ; :: thesis: AS is Fanoian
set XX = IncProjSp_of AS;
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 & a,c // b,d ) and
A3: a,d // b,c ; :: thesis: a,b // a,c
assume A4: not a,b // a,c ; :: thesis: contradiction
reconsider p = a, q = d, r = c, s = b as Element of the Points of (IncProjSp_of AS) by Th20;
A5: ( a <> b & a <> c & b <> c ) by A4, AFF_1:11, AFF_1:12;
A6: ( a in Line a,b & b in Line a,b & c in Line c,d & d in Line c,d & b in Line b,d & d in Line b,d & a in Line a,c & c in Line a,c & a in Line a,d & d in Line a,d & b in Line b,c & c in Line b,c ) by AFF_1:26;
A7: ( Line a,b <> Line c,d & Line a,c <> Line b,d )
proof
A8: now
assume Line a,b = Line c,d ; :: thesis: contradiction
then LIN a,b,c by A6, AFF_1:def 2;
hence contradiction by A4, AFF_1:def 1; :: thesis: verum
end;
now
assume Line a,c = Line b,d ; :: thesis: contradiction
then LIN a,c,b by A6, AFF_1:def 2;
then LIN a,b,c by AFF_1:15;
hence contradiction by A4, AFF_1:def 1; :: thesis: verum
end;
hence ( Line a,b <> Line c,d & Line a,c <> Line b,d ) by A8; :: thesis: verum
end;
A9: ( c <> d & b <> d & a <> d )
proof
A10: now
assume c = d ; :: thesis: contradiction
then c,a // c,b by A2, AFF_1:13;
then LIN c,a,b by AFF_1:def 1;
then LIN a,b,c by AFF_1:15;
hence contradiction by A4, AFF_1:def 1; :: thesis: verum
end;
hence ( c <> d & b <> d & a <> d ) by A2, A4, A10, AFF_1:13; :: thesis: verum
end;
then A11: ( Line a,b is being_line & Line c,d is being_line & Line b,d is being_line & Line a,c is being_line & Line a,d is being_line & Line b,c is being_line ) by A5, AFF_1:def 3;
A12: ( Line a,b // Line c,d & Line a,c // Line b,d & Line a,d // Line b,c ) by A2, A3, A5, A9, AFF_1:51;
then A13: ( Line a,b '||' Line c,d & Line a,c '||' Line b,d & Line a,d '||' Line b,c ) by A11, AFF_4:40;
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 A11, Th23;
reconsider a' = LDir (Line a,b), b' = LDir (Line a,c), c' = LDir (Line a,d) as Element of the Points of (IncProjSp_of AS) by A11, Th20;
consider Y being Subset of AS such that
A14: ( Line a,b c= Y & Line a,c c= Y ) and
A15: Y is being_plane by A6, A11, AFF_4:38;
reconsider C1 = [(PDir Y),2] as Element of the Lines of (IncProjSp_of AS) by A15, Th23;
A16: ( Line a,b c= Y & Line a,c c= Y & Line a,d c= Y )
proof
thus ( Line a,b c= Y & Line a,c c= Y ) by A14; :: thesis: Line a,d c= Y
Line b,d = b * (Line a,c) by A6, A11, A12, AFF_4:def 3;
then Line b,d c= Y by A6, A11, A14, A15, AFF_4:28;
hence Line a,d c= Y by A6, A9, A14, A15, AFF_4:19; :: thesis: verum
end;
A17: ( p on L1 & s on L1 & a' on L1 & r on Q1 & q on Q1 & a' on Q1 & p on S1 & r on S1 & b' on S1 & s on R1 & q on R1 & b' on R1 ) by A6, A11, A13, Th26, Th28, Th30;
A18: ( p on A1 & q on A1 & c' on A1 & r on B1 & s on B1 & c' on B1 ) by A6, A11, A13, Th26, Th28, Th30;
A19: ( a' on C1 & b' on C1 & c' on C1 ) by A11, A15, A16, Th31;
A20: ( not q on L1 & not r on L1 & not p on Q1 & not s on Q1 & not p on R1 & not r on R1 & not q on S1 & not s on S1 )
proof
A21: now
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 A6, A7, A12, AFF_1:59; :: thesis: verum
end;
A22: now
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 A6, A7, A12, AFF_1:59; :: thesis: verum
end;
A23: now
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 A6, A7, A12, AFF_1:59; :: thesis: verum
end;
now
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 A6, A7, A12, AFF_1:59; :: thesis: verum
end;
hence ( not q on L1 & not r on L1 & not p on Q1 & not s on Q1 & not p on R1 & not r on R1 & not q on S1 & not s on S1 ) by A21, A22, A23; :: thesis: verum
end;
A24: ( {a',p,s} on L1 & {a',q,r} on Q1 & {b',q,s} on R1 & {b',p,r} on S1 & {c',p,q} on A1 & {c',r,s} on B1 ) by A17, A18, INCSP_1:12;
{a',b'} on C1 by A19, INCSP_1:11;
hence contradiction by A1, A19, A20, A24, INCPROJ:def 18; :: thesis: verum
end;
hence AS is Fanoian by PAPDESAF:def 5; :: thesis: verum