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

for A being being_line Subset of AS holds

( a,b // A iff 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 being_line Subset of AS holds

( a,b // A iff ex c, d being Element of AS st

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

A1: 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 ) by Th27;

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

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

( ex c, d being Element of AS st

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

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

for A being being_line Subset of AS holds

( a,b // A iff 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 being_line Subset of AS holds

( a,b // A iff ex c, d being Element of AS st

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

A1: 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 ) by Th27;

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

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

( ex c, d being Element of AS st

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

proof

hence
( a,b // A iff ex c, d being Element of AS st
assume
ex c, d being Element of AS st

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

then consider c, d being Element of AS such that

A2: c <> d and

A3: c in A and

A4: d in A and

A5: a,b // c,d ;

A = Line (c,d) by A2, A3, A4, Lm6;

hence a,b // A by A2, A5; :: thesis: verum

end;( c <> d & c in A & d in A & a,b // c,d ) ; :: thesis: a,b // A

then consider c, d being Element of AS such that

A2: c <> d and

A3: c in A and

A4: d in A and

A5: a,b // c,d ;

A = Line (c,d) by A2, A3, A4, Lm6;

hence a,b // A by A2, A5; :: thesis: verum

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