let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st ex p, q being POINT of S st p <> q holds
( Collinear a,b,c iff ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) )
let a, b, c be POINT of S; :: thesis: ( ex p, q being POINT of S st p <> q implies ( Collinear a,b,c iff ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) ) )
assume ex p, q being POINT of S st p <> q ; :: thesis: ( Collinear a,b,c iff ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) )
then consider p, q being POINT of S such that
A1: p <> q ;
A2: ( ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) implies Collinear a,b,c )
proof
assume ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) ; :: thesis: Collinear a,b,c
then consider A being Subset of S such that
A3: A is_line and
A4: a in A and
A5: b in A and
A6: c in A ;
per cases ( a <> b or a = b ) ;
suppose a <> b ; :: thesis: Collinear a,b,c
then c in Line (a,b) by A3, A4, A5, A6, Satz6p18;
then ex x being POINT of S st
( c = x & Collinear a,b,x ) ;
hence Collinear a,b,c ; :: thesis: verum
end;
end;
end;
( Collinear a,b,c implies ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) )
proof
assume A8: Collinear a,b,c ; :: thesis: ex A being Subset of S st
( A is_line & a in A & b in A & c in A )
per cases ( a = b or a <> b ) ;
suppose A9: a = b ; :: thesis: ex A being Subset of S st
( A is_line & a in A & b in A & c in A )
per cases ( a = c or a <> c ) ;
suppose A10: a = c ; :: thesis: ex A being Subset of S st
( A is_line & a in A & b in A & c in A )
per cases ( a <> p or a <> q ) by A1;
suppose A11: a <> p ; :: thesis: ex A being Subset of S st
( A is_line & a in A & b in A & c in A )
set A = Line (a,p);
now :: thesis: ( Line (a,p) is_line & a in Line (a,p) & b in Line (a,p) & c in Line (a,p) )
thus Line (a,p) is_line by A11; :: thesis: ( a in Line (a,p) & b in Line (a,p) & c in Line (a,p) )
Collinear a,p,a by Satz3p1;
hence ( a in Line (a,p) & b in Line (a,p) & c in Line (a,p) ) by A9, A10; :: thesis: verum
end;
hence ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) ; :: thesis: verum
end;
suppose A12: a <> q ; :: thesis: ex A being Subset of S st
( A is_line & a in A & b in A & c in A )
set A = Line (a,q);
now :: thesis: ( Line (a,q) is_line & a in Line (a,q) & b in Line (a,q) & c in Line (a,q) )
thus Line (a,q) is_line by A12; :: thesis: ( a in Line (a,q) & b in Line (a,q) & c in Line (a,q) )
Collinear a,q,a by Satz3p1;
hence ( a in Line (a,q) & b in Line (a,q) & c in Line (a,q) ) by A9, A10; :: thesis: verum
end;
hence ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) ; :: thesis: verum
end;
end;
end;
suppose A13: a <> c ; :: thesis: ex A being Subset of S st
( A is_line & a in A & b in A & c in A )
set A = Line (a,c);
now :: thesis: ( Line (a,c) is_line & a in Line (a,c) & b in Line (a,c) & c in Line (a,c) )
thus Line (a,c) is_line by A13; :: thesis: ( a in Line (a,c) & b in Line (a,c) & c in Line (a,c) )
( Collinear a,c,a & Collinear a,c,c ) by Satz3p1;
hence ( a in Line (a,c) & b in Line (a,c) & c in Line (a,c) ) by A9; :: thesis: verum
end;
hence ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) ; :: thesis: verum
end;
end;
end;
suppose A14: a <> b ; :: thesis: ex A being Subset of S st
( A is_line & a in A & b in A & c in A )
( Collinear a,b,a & Collinear a,b,b ) by Satz3p1;
then A15: ( a in Line (a,b) & b in Line (a,b) & c in Line (a,b) ) by A8;
reconsider A = Line (a,b) as Subset of S ;
A is_line by A14;
hence ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) by A15; :: thesis: verum
end;
end;
end;
hence ( Collinear a,b,c iff ex A being Subset of S st
( A is_line & a in A & b in A & c in A ) ) by A2; :: thesis: verum