let SAS be Semi_Affine_Space; :: thesis: for o, b, a, d, c being Element of SAS holds
( o, diff b,a,o, diff d,c,o is_collinear iff a,b // c,d )
let o, b, a, d, c be Element of SAS; :: thesis: ( o, diff b,a,o, diff d,c,o is_collinear iff a,b // c,d )
A1: ( o, diff b,a,o, diff d,c,o is_collinear implies a,b // c,d )

proof

assume A2: o, diff b,a,o, diff d,c,o is_collinear ; :: thesis: a,b // c,d

A3: now

assume ( o = diff b,a,o or o = diff d,c,o ) ; :: thesis: a,b // c,d
then ( a = b or c = d ) by Th113;
hence a,b // c,d by Def1, Th14; :: thesis: verum

end;

now

assume ( o <> diff b,a,o & o <> diff d,c,o ) ; :: thesis: a,b // c,d
then ( o <> diff b,a,o & o <> diff d,c,o & o, diff b,a,o // o, diff d,c,o & o, diff b,a,o // a,b & o, diff d,c,o // c,d & o <> diff d,c,o ) by A2, Def2, Th114;
then ( o <> diff d,c,o & o, diff d,c,o // a,b & o, diff d,c,o // c,d ) by Def1;
hence a,b // c,d by Def1; :: thesis: verum

end;

hence a,b // c,d by A3; :: thesis: verum

end;

( a,b // c,d implies o, diff b,a,o, diff d,c,o is_collinear )

proof

assume A4: a,b // c,d ; :: thesis: o, diff b,a,o, diff d,c,o is_collinear

A5: now

assume ( a = b or c = d ) ; :: thesis: o, diff b,a,o, diff d,c,o is_collinear
then ( o = diff b,a,o or o = diff d,c,o ) by Th113;
then o, diff b,a,o // o, diff d,c,o by Def1, Th14;
hence o, diff b,a,o, diff d,c,o is_collinear by Def2; :: thesis: verum

end;

now

assume ( a <> b & c <> d ) ; :: thesis: o, diff b,a,o, diff d,c,o is_collinear
then ( a <> b & c <> d & o, diff b,a,o // a,b & o, diff d,c,o // c,d ) by Th114;
then ( a <> b & c <> d & a,b // o, diff b,a,o & c,d // o, diff d,c,o & a,b // c,d ) by A4, Th17;
then ( o, diff b,a,o // c,d & c,d // o, diff d,c,o & c <> d ) by Def1;
then o, diff b,a,o // o, diff d,c,o by Th20;
hence o, diff b,a,o, diff d,c,o is_collinear by Def2; :: thesis: verum

end;

hence o, diff b,a,o, diff d,c,o is_collinear by A5; :: thesis: verum

end;

hence ( o, diff b,a,o, diff d,c,o is_collinear iff a,b // c,d ) by A1; :: thesis: verum