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;

now :: thesis: ( a <> a9 implies 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;

hence ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 ) by A3, AFF_1:2; :: thesis: verum