let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d, p being POINT of S st not Collinear a,b,c & b <> d & a,b equiv c,d & b,c equiv d,a & Collinear a,p,c & Collinear b,p,d holds
( Middle a,p,c & Middle b,p,d )
let a, b, c, d, p be POINT of S; :: thesis: ( not Collinear a,b,c & b <> d & a,b equiv c,d & b,c equiv d,a & Collinear a,p,c & Collinear b,p,d implies ( Middle a,p,c & Middle b,p,d ) )
assume that
A1: not Collinear a,b,c and
A2: b <> d and
A3: a,b equiv c,d and
A4: b,c equiv d,a and
A5: Collinear a,p,c and
A6: Collinear b,p,d ; :: thesis: ( Middle a,p,c & Middle b,p,d )
A7: Collinear b,d,p by A6, Satz3p2;
then consider p9 being POINT of S such that
A8: b,d,p cong d,b,p9 by GTARSKI1:def 5, Satz4p14;
A9: Collinear d,b,p9 by A7, A8, Satz4p13;
now :: thesis: ( Collinear b,d,p & b,d,p cong d,b,p9 & b,a equiv d,c & d,a equiv b,c )
thus Collinear b,d,p by A6, Satz3p2; :: thesis: ( b,d,p cong d,b,p9 & b,a equiv d,c & d,a equiv b,c )
thus b,d,p cong d,b,p9 by A8; :: thesis: ( b,a equiv d,c & d,a equiv b,c )
a,b equiv d,c by A3, Satz2p5;
hence b,a equiv d,c by Satz2p4; :: thesis: d,a equiv b,c
thus d,a equiv b,c by A4, Satz2p2; :: thesis: verum
end;
then A10: b,d,p,a FS d,b,p9,c ;
then p,a equiv c,p9 by A2, Satz4p16, Satz2p5;
then A11: a,p equiv c,p9 by Satz2p4;
A12: a,c equiv c,a by GTARSKI1:def 5;
now :: thesis: ( Collinear b,d,p & b,d,p cong d,b,p9 & b,c equiv d,a & d,c equiv b,a )
thus Collinear b,d,p by A6, Satz3p2; :: thesis: ( b,d,p cong d,b,p9 & b,c equiv d,a & d,c equiv b,a )
thus b,d,p cong d,b,p9 by A8; :: thesis: ( b,c equiv d,a & d,c equiv b,a )
thus b,c equiv d,a by A4; :: thesis: d,c equiv b,a
a,b equiv d,c by A3, Satz2p5;
then b,a equiv d,c by Satz2p4;
hence d,c equiv b,a by Satz2p2; :: thesis: verum
end;
then b,d,p,c FS d,b,p9,a ;
then p,c equiv p9,a by A2, Satz4p16;
then A13: Collinear c,p9,a by A5, Satz4p13, A11, A12, GTARSKI1:def 3;
A14: a <> c by A1, Satz3p1;
A15: Line (a,c) <> Line (b,d)
proof
assume Line (a,c) = Line (b,d) ; :: thesis: contradiction
then b in Line (a,c) by Satz6p17;
then ex x being POINT of S st
( b = x & Collinear a,c,x ) ;
hence contradiction by A1, Satz3p2; :: thesis: verum
end;
now :: thesis: ( Line (a,c) <> Line (b,d) & Line (a,c) is_line & Line (b,d) is_line & p9 in Line (a,c) & p9 in Line (b,d) & p in Line (a,c) & p in Line (b,d) )
thus Line (a,c) <> Line (b,d) by A15; :: thesis: ( Line (a,c) is_line & Line (b,d) is_line & p9 in Line (a,c) & p9 in Line (b,d) & p in Line (a,c) & p in Line (b,d) )
thus Line (a,c) is_line by A14; :: thesis: ( Line (b,d) is_line & p9 in Line (a,c) & p9 in Line (b,d) & p in Line (a,c) & p in Line (b,d) )
thus Line (b,d) is_line by A2; :: thesis: ( p9 in Line (a,c) & p9 in Line (b,d) & p in Line (a,c) & p in Line (b,d) )
Collinear a,c,p9 by A13;
hence p9 in Line (a,c) ; :: thesis: ( p9 in Line (b,d) & p in Line (a,c) & p in Line (b,d) )
Collinear b,d,p9 by A9, Satz3p2;
hence p9 in Line (b,d) ; :: thesis: ( p in Line (a,c) & p in Line (b,d) )
Collinear a,c,p by A5, Satz3p2;
hence p in Line (a,c) ; :: thesis: p in Line (b,d)
Collinear b,d,p by A6, Satz3p2;
hence p in Line (b,d) ; :: thesis: verum
end;
then A16: p9 = p by Satz6p19;
now :: thesis: ( Middle a,p,c & Middle b,p,d )
thus Middle a,p,c by A14, Satz7p20, A10, A2, Satz4p16, A16, A5; :: thesis: Middle b,p,d
b,p equiv p,d by A16, A8, Satz2p5;
hence Middle b,p,d by A2, Satz7p20, A6, Satz2p4; :: thesis: verum
end;
hence ( Middle a,p,c & Middle b,p,d ) ; :: thesis: verum