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

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