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

for A being Subset of AS st a,b // A holds

ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

let a, b be Element of AS; :: thesis: for A being Subset of AS st a,b // A holds

ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

let A be Subset of AS; :: thesis: ( a,b // A implies ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d ) )

assume a,b // A ; :: thesis: ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

then consider c, d being Element of AS such that

A1: c <> d and

A2: A = Line (c,d) and

A3: a,b // c,d ;

A4: d in A by A2, Th14;

c in A by A2, Th14;

hence ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d ) by A1, A3, A4; :: thesis: verum

for A being Subset of AS st a,b // A holds

ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

let a, b be Element of AS; :: thesis: for A being Subset of AS st a,b // A holds

ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

let A be Subset of AS; :: thesis: ( a,b // A implies ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d ) )

assume a,b // A ; :: thesis: ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d )

then consider c, d being Element of AS such that

A1: c <> d and

A2: A = Line (c,d) and

A3: a,b // c,d ;

A4: d in A by A2, Th14;

c in A by A2, Th14;

hence ex c, d being Element of AS st

( c <> d & c in A & d in A & a,b // c,d ) by A1, A3, A4; :: thesis: verum