let AS be AffinSpace; 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; 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; ( 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
; 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 ( a <> a9 implies ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 ) )assume A5:
a <> a9
;
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;
verum end;
hence
ex d9 being Element of AS st
( d9 in K & a,d // a9,d9 )
by A3, AFF_1:2; verum