let OAS be OAffinSpace; :: thesis: for p, a, b, c being Element of OAS st not LIN p,a,b & p,a '||' b,c & p,b '||' a,c holds
( p,a // b,c & p,b // a,c )
let p, a, b, c be Element of OAS; :: thesis: ( not LIN p,a,b & p,a '||' b,c & p,b '||' a,c implies ( p,a // b,c & p,b // a,c ) )
assume A1: ( not LIN p,a,b & p,a '||' b,c & p,b '||' a,c ) ; :: thesis: ( p,a // b,c & p,b // a,c )
consider d being Element of OAS such that
A2: p,a // b,d and
A3: p,b // a,d and
a <> d by ANALOAF:def 5;
( p,a '||' b,d & p,b '||' a,d ) by A2, A3, DIRAF:def 4;
hence ( p,a // b,c & p,b // a,c ) by A1, A2, A3, Th12; :: thesis: verum