let OAS be OAffinSpace; :: thesis: for a, b, c being Element of OAS
for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( a,b,c are_collinear iff LIN a9,b9,c9 )
let a, b, c be Element of OAS; :: thesis: for a9, b9, c9 being Element of (Lambda OAS) st a = a9 & b = b9 & c = c9 holds
( a,b,c are_collinear iff LIN a9,b9,c9 )
let a9, b9, c9 be Element of (Lambda OAS); :: thesis: ( a = a9 & b = b9 & c = c9 implies ( a,b,c are_collinear iff LIN a9,b9,c9 ) )
assume A1: ( a = a9 & b = b9 & c = c9 ) ; :: thesis: ( a,b,c are_collinear iff LIN a9,b9,c9 )

A2: now :: thesis: ( a,b,c are_collinear implies LIN a9,b9,c9 )

assume a,b,c are_collinear ; :: thesis: LIN a9,b9,c9
then a,b '||' a,c by DIRAF:def 5;
then a9,b9 // a9,c9 by A1, DIRAF:38;
hence LIN a9,b9,c9 by AFF_1:def 1; :: thesis: verum

end;

now :: thesis: ( LIN a9,b9,c9 implies a,b,c are_collinear )

assume LIN a9,b9,c9 ; :: thesis: a,b,c are_collinear
then a9,b9 // a9,c9 by AFF_1:def 1;
then a,b '||' a,c by A1, DIRAF:38;
hence a,b,c are_collinear by DIRAF:def 5; :: thesis: verum

end;

hence ( a,b,c are_collinear iff LIN a9,b9,c9 ) by A2; :: thesis: verum