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