let n be Nat; :: thesis: for An, Bn, Cn being Point of (TOP-REAL n)
for Ln being Element of line_of_REAL n st An <> Cn & Cn in LSeg (An,Bn) & An in Ln & Cn in Ln & Ln is being_line holds
Bn in Ln
let An, Bn, Cn be Point of (TOP-REAL n); :: thesis: for Ln being Element of line_of_REAL n st An <> Cn & Cn in LSeg (An,Bn) & An in Ln & Cn in Ln & Ln is being_line holds
Bn in Ln
let Ln be Element of line_of_REAL n; :: thesis: ( An <> Cn & Cn in LSeg (An,Bn) & An in Ln & Cn in Ln & Ln is being_line implies Bn in Ln )
assume that
A1: An <> Cn and
A2: Cn in LSeg (An,Bn) and
A3: An in Ln and
A4: Cn in Ln and
A5: Ln is being_line ; :: thesis: Bn in Ln
reconsider rAn = An, rCn = Cn, rBn = Bn as Element of REAL n by EUCLID:22;
Line (rAn,rCn) = Ln by A1, A3, A4, A5, EUCLIDLP:30;
then A6: Line (An,Cn) = Ln by Th4;
LSeg (An,Bn) c= Line (An,Bn) by RLTOPSP1:73;
then A7: ( Cn in Line (An,Bn) & An in Line (An,Bn) & An <> Cn ) by A1, A2, EUCLID_4:41;
( Line (rAn,rBn) = Line (An,Bn) & Line (rAn,rCn) = Line (An,Cn) ) by Th4;
then Line (An,Bn) c= Line (An,Cn) by A7, EUCLID_4:11;
hence Bn in Ln by A6, EUCLID_4:41; :: thesis: verum