let AS be AffinSpace; :: thesis: for a, b, a9, p being Element of AS st ( LIN p,a,a9 or LIN p,a9,a ) & p <> a holds
ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 )
let a, b, a9, p be Element of AS; :: thesis: ( ( LIN p,a,a9 or LIN p,a9,a ) & p <> a implies ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 ) )
assume that
A1: ( LIN p,a,a9 or LIN p,a9,a ) and
A2: p <> a ; :: thesis: ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 )
LIN p,a,a9 by A1, AFF_1:6;
then p,a // p,a9 by AFF_1:def 1;
then a,p // p,a9 by AFF_1:4;
then consider b9 being Element of AS such that
A3: b,p // p,b9 and
A4: b,a // a9,b9 by A2, DIRAF:40;
p,b // p,b9 by A3, AFF_1:4;
then A5: LIN p,b,b9 by AFF_1:def 1;
a,b // a9,b9 by A4, AFF_1:4;
hence ex b9 being Element of AS st
( LIN p,b,b9 & a,b // a9,b9 ) by A5; :: thesis: verum