let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st Collinear a,b,c holds
( between a,b,c iff ( a,b <= a,c & b,c <= a,c ) )
let a, b, c be POINT of S; :: thesis: ( Collinear a,b,c implies ( between a,b,c iff ( a,b <= a,c & b,c <= a,c ) ) )
assume A1: Collinear a,b,c ; :: thesis: ( between a,b,c iff ( a,b <= a,c & b,c <= a,c ) )
thus ( between a,b,c implies ( a,b <= a,c & b,c <= a,c ) ) :: thesis: ( a,b <= a,c & b,c <= a,c implies between a,b,c )
proof
assume A2: between a,b,c ; :: thesis: ( a,b <= a,c & b,c <= a,c )
hence a,b <= a,c by Satz2p1; :: thesis: b,c <= a,c
thus b,c <= a,c :: thesis: verum
proof
between c,b,a by A2, Satz3p2;
then c,b <= c,a by Satz2p1;
then b,c <= c,a by Satz2p4;
hence b,c <= a,c by Lemma5p12p2; :: thesis: verum
end;
end;
thus ( a,b <= a,c & b,c <= a,c implies between a,b,c ) :: thesis: verum
proof
assume A3: ( a,b <= a,c & b,c <= a,c ) ; :: thesis: between a,b,c
A4: ( between c,a,b implies between a,b,c )
proof
assume A5: between c,a,b ; :: thesis: between a,b,c
c,b <= a,c by A3, Satz2p4;
then a = b by A5, Lemma5p12p2, Lemma5p12p4;
hence between a,b,c by Satz3p1, Satz3p2; :: thesis: verum
end;
( between b,c,a implies between a,b,c )
proof
assume between b,c,a ; :: thesis: between a,b,c
then b = c by A3, Satz3p2, Lemma5p12p4;
hence between a,b,c by Satz3p1; :: thesis: verum
end;
hence between a,b,c by A1, A4; :: thesis: verum
end;