let AS be AffinSpace; :: thesis: for a, a', d being Element of
for A, K being Subset of st A // K & a in A & a' in A & d in K holds
ex d' being Element of st
( d' in K & a,d // a',d' )
let a, a', d be Element of ; :: thesis: for A, K being Subset of st A // K & a in A & a' in A & d in K holds
ex d' being Element of st
( d' in K & a,d // a',d' )
let A, K be Subset of ; :: thesis: ( A // K & a in A & a' in A & d in K implies ex d' being Element of st
( d' in K & a,d // a',d' ) )
assume that
A1: A // K and
A2: ( a in A & a' in A ) and
A3: d in K ; :: thesis: ex d' being Element of st
( d' in K & a,d // a',d' )
A4: A is being_line by A1, AFF_1:50;

now

assume A5: a <> a' ; :: thesis: ex d' being Element of st
( d' in K & a,d // a',d' )
consider d' being Element of such that
A6: a,a' // d,d' and
A7: a,d // a',d' by DIRAF:47;
d,d' // a,a' by A6, AFF_1:13;
then d,d' // A by A2, A4, A5, AFF_1:41;
then d,d' // K by A1, Th3;
then d' in K by A3, Th2;
hence ex d' being Element of st
( d' in K & a,d // a',d' ) by A7; :: thesis: verum

end;

hence ex d' being Element of st
( d' in K & a,d // a',d' ) by A3, AFF_1:11; :: thesis: verum