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