let AS be AffinSpace; :: thesis: for a, b, x being Element of AS

for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds

x in A

let a, b, x be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds

x in A

let A be Subset of AS; :: thesis: ( A is being_line & a in A & b in A & a <> b & LIN a,b,x implies x in A )

assume that

A1: A is being_line and

A2: a in A and

A3: b in A and

A4: a <> b and

A5: LIN a,b,x ; :: thesis: x in A

A = Line (a,b) by A1, A2, A3, A4, Lm6;

hence x in A by A5, Def2; :: thesis: verum

for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds

x in A

let a, b, x be Element of AS; :: thesis: for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds

x in A

let A be Subset of AS; :: thesis: ( A is being_line & a in A & b in A & a <> b & LIN a,b,x implies x in A )

assume that

A1: A is being_line and

A2: a in A and

A3: b in A and

A4: a <> b and

A5: LIN a,b,x ; :: thesis: x in A

A = Line (a,b) by A1, A2, A3, A4, Lm6;

hence x in A by A5, Def2; :: thesis: verum