let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st c,a equiv c,b holds
ex x being POINT of S st Middle a,x,b
let a, b, c be POINT of S; :: thesis: ( c,a equiv c,b implies ex x being POINT of S st Middle a,x,b )
assume A1: c,a equiv c,b ; :: thesis: ex x being POINT of S st Middle a,x,b
per cases ( Collinear a,b,c or not Collinear a,b,c ) ;
suppose Collinear a,b,c ; :: thesis: ex x being POINT of S st Middle a,x,b
then Collinear a,c,b by Satz3p2;
per cases then ( a = b or Middle a,c,b ) by A1, Satz7p20;
suppose A2: a = b ; :: thesis: ex x being POINT of S st Middle a,x,b
take a ; :: thesis: Middle a,a,b
thus Middle a,a,b by A2, Satz3p1, Satz2p1; :: thesis: verum
end;
suppose Middle a,c,b ; :: thesis: ex x being POINT of S st Middle a,x,b
hence ex x being POINT of S st Middle a,x,b ; :: thesis: verum
end;
end;
end;
suppose A3: not Collinear a,b,c ; :: thesis: ex x being POINT of S st Middle a,x,b
consider p being POINT of S such that
A4: between c,a,p and
A5: a <> p by Satz3p14;
consider q being POINT of S such that
A6: between c,b,q and
A7: b,q equiv a,p by GTARSKI1:def 8;
( between p,a,c & between q,b,c ) by A4, A6, Satz3p2;
then consider r being POINT of S such that
A8: between a,r,q and
A9: between b,r,p by GTARSKI1:def 11;
consider x being POINT of S such that
A10: between a,x,b and
A11: between r,x,c by A4, A9, GTARSKI1:def 11;
take x ; :: thesis: Middle a,x,b
x,a equiv x,b
proof
A12: r,a equiv r,b
proof
A13: c,a,p,b AFS c,b,q,a by A4, A6, A1, A7, GTARSKI1:def 5, Satz2p2;
c <> a by A3, Satz3p1;
then A15: p,b equiv a,q by Satz2p5, A13, Axiom5AFS;
r,a equiv r,b
proof
consider r9 being POINT of S such that
A19: between a,r9,q and
A20: b,r,p cong a,r9,q by A15, Satz2p4, A9, Satz4p5;
A21: now :: thesis: ( b,r,p,a IFS a,r9,q,b & b,r,p,q IFS a,r9,q,p )
b,q equiv p,a by A7, Satz2p5;
then q,b equiv p,a by Satz2p4;
hence b,r,p,a IFS a,r9,q,b by A9, A19, A20, Satz2p2, GTARSKI1:def 5; :: thesis: b,r,p,q IFS a,r9,q,p
thus b,r,p,q IFS a,r9,q,p by A9, A19, A20, GTARSKI1:def 5, A7; :: thesis: verum
end;
then r,a equiv b,r9 by Satz2p5, Satz4p2;
then A23: a,r,q cong b,r9,p by A21, Satz2p4, Satz2p2, Satz4p2;
now :: thesis: ( Collinear a,r,q & Collinear b,r9,p )
thus Collinear a,r,q by A8; :: thesis: Collinear b,r9,p
hence Collinear b,r9,p by A23, Satz4p13; :: thesis: verum
end;
then ( Collinear a,q,r & Collinear b,p,r9 ) by Satz3p2;
then A24: ( r in Line (a,q) & r9 in Line (b,p) ) ;
A25: ( r9 in Line (a,q) & r in Line (b,p) )
proof
Collinear a,q,r9 by A19, Satz3p2;
hence r9 in Line (a,q) ; :: thesis: r in Line (b,p)
Collinear b,p,r by A9, Satz3p2;
hence r in Line (b,p) ; :: thesis: verum
end;
A26: ( a = q iff b = p ) by A15, Satz2p2, GTARSKI1:def 7;
r = r9
proof
per cases ( a = q or b = p or ( a <> q & b <> p ) ) ;
suppose A29: ( a <> q & b <> p ) ; :: thesis: r = r9
assume A30: r <> r9 ; :: thesis: contradiction
reconsider A = Line (a,q), B = Line (b,p) as Subset of S ;
A31: ( A is_line & B is_line ) by A29;
then A32: A = B by A30, A24, A25, Satz6p19;
A33: a <> b by A3, Satz3p1;
A34: A = Line (a,b)
proof
( b in A & a in A & A is_line ) by A29, A32, Satz6p17;
hence A = Line (a,b) by A33, Satz6p18; :: thesis: verum
end;
A35: Line (a,p) = A
proof
A36: a in A by Satz6p17;
p in B by Satz6p17;
then ( p in A & A is_line ) by A31, A30, A24, A25, Satz6p19;
hence Line (a,p) = A by A36, A5, Satz6p18; :: thesis: verum
end;
c in A
proof
Collinear a,p,c by A4;
hence c in A by A35; :: thesis: verum
end;
then ex y being POINT of S st
( c = y & Collinear a,b,y ) by A34;
hence contradiction by A3; :: thesis: verum
end;
end;
end;
hence r,a equiv r,b by A21, Satz4p2; :: thesis: verum
end;
hence r,a equiv r,b ; :: thesis: verum
end;
per cases ( r = c or r <> c ) ;
suppose A37: r <> c ; :: thesis: x,a equiv x,b
( Collinear c,r,x & c,a equiv c,b & r,a equiv r,b ) by A11, A1, A12;
hence x,a equiv x,b by A37, Satz4p17; :: thesis: verum
end;
end;
end;
hence Middle a,x,b by A10; :: thesis: verum
end;
end;