let OAS be OAffinSpace; 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; 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); ( 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 )
; ( a,b,c are_collinear iff LIN a9,b9,c9 )
A2:
now ( a,b,c are_collinear implies LIN a9,b9,c9 )assume
a,
b,
c are_collinear
;
LIN a9,b9,c9then
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;
verum end;
now ( LIN a9,b9,c9 implies a,b,c are_collinear )assume
LIN a9,
b9,
c9
;
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;
verum end;
hence
( a,b,c are_collinear iff LIN a9,b9,c9 )
by A2; verum