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

for A, K being Subset of AS st A // K & a in A & a9 in A & d in K holds

ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

let a, d, a9 be Element of AS; :: thesis: for A, K being Subset of AS st A // K & a in A & a9 in A & d in K holds

ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

let A, K be Subset of AS; :: thesis: ( A // K & a in A & a9 in A & d in K implies ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 ) )

assume that

A1: A // K and

A2: ( a in A & a9 in A ) and

A3: d in K ; :: thesis: ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

A4: A is being_line by A1, AFF_1:36;

( d9 in K & a,d // a9,d9 ) by A3, AFF_1:2; :: thesis: verum

for A, K being Subset of AS st A // K & a in A & a9 in A & d in K holds

ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

let a, d, a9 be Element of AS; :: thesis: for A, K being Subset of AS st A // K & a in A & a9 in A & d in K holds

ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

let A, K be Subset of AS; :: thesis: ( A // K & a in A & a9 in A & d in K implies ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 ) )

assume that

A1: A // K and

A2: ( a in A & a9 in A ) and

A3: d in K ; :: thesis: ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

A4: A is being_line by A1, AFF_1:36;

now :: thesis: ( a <> a9 implies ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 ) )

hence
ex d9 being Element of AS st ( d9 in K & a,d // a9,d9 ) )

assume A5:
a <> a9
; :: thesis: ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 )

consider d9 being Element of AS such that

A6: a,a9 // d,d9 and

A7: a,d // a9,d9 by DIRAF:40;

d,d9 // a,a9 by A6, AFF_1:4;

then d,d9 // A by A2, A4, A5, AFF_1:27;

then d,d9 // K by A1, Th3;

then d9 in K by A3, Th2;

hence ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 ) by A7; :: thesis: verum

end;( d9 in K & a,d // a9,d9 )

consider d9 being Element of AS such that

A6: a,a9 // d,d9 and

A7: a,d // a9,d9 by DIRAF:40;

d,d9 // a,a9 by A6, AFF_1:4;

then d,d9 // A by A2, A4, A5, AFF_1:27;

then d,d9 // K by A1, Th3;

then d9 in K by A3, Th2;

hence ex d9 being Element of AS st

( d9 in K & a,d // a9,d9 ) by A7; :: thesis: verum

( d9 in K & a,d // a9,d9 ) by A3, AFF_1:2; :: thesis: verum