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

for A being Subset of AS st A is being_line & a in A holds

( b in A iff a,b // A )

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

( b in A iff a,b // A )

let A be Subset of AS; :: thesis: ( A is being_line & a in A implies ( b in A iff a,b // A ) )

assume that

A1: A is being_line and

A2: a in A ; :: thesis: ( b in A iff a,b // A )

consider p, q being Element of AS such that

A3: p <> q and

A4: A = Line (p,q) by A1;

then consider p, q being Element of AS such that

A5: p <> q and

A6: A = Line (p,q) and

A7: a,b // p,q ;

p,q // a,b by A7, Th3;

hence b in A by A2, A5, A6, Th21; :: thesis: verum

for A being Subset of AS st A is being_line & a in A holds

( b in A iff a,b // A )

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

( b in A iff a,b // A )

let A be Subset of AS; :: thesis: ( A is being_line & a in A implies ( b in A iff a,b // A ) )

assume that

A1: A is being_line and

A2: a in A ; :: thesis: ( b in A iff a,b // A )

consider p, q being Element of AS such that

A3: p <> q and

A4: A = Line (p,q) by A1;

hereby :: thesis: ( a,b // A implies b in A )

assume
a,b // A
; :: thesis: b in Aassume
b in A
; :: thesis: a,b // A

then p,q // a,b by A2, A3, A4, Th21;

then a,b // p,q by Th3;

hence a,b // A by A3, A4; :: thesis: verum

end;then p,q // a,b by A2, A3, A4, Th21;

then a,b // p,q by Th3;

hence a,b // A by A3, A4; :: thesis: verum

then consider p, q being Element of AS such that

A5: p <> q and

A6: A = Line (p,q) and

A7: a,b // p,q ;

p,q // a,b by A7, Th3;

hence b in A by A2, A5, A6, Th21; :: thesis: verum