let n be Nat; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n) st An <> Cn & An in Line (Bn,Cn) holds
Bn in Line (An,Cn)
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: ( An <> Cn & An in Line (Bn,Cn) implies Bn in Line (An,Cn) )
assume that
A1: An <> Cn and
A2: An in Line (Bn,Cn) ; :: thesis: Bn in Line (An,Cn)
Cn in Line (Bn,Cn) by EUCLID_4:41;
then Line (Bn,Cn) c= Line (An,Cn) by A1, A2, EUCLID_4:43;
hence Bn in Line (An,Cn) by EUCLID_4:41; :: thesis: verum