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: ( a,b // c,d implies o, diff b,a,o, diff d,c,o is_collinear )

proof

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

A3: now

o, diff d,c,o // c,d by Th114;
then A4: c,d // o, diff d,c,o by Th17;
assume that
A5: a <> b and
A6: c <> d ; :: thesis: o, diff b,a,o, diff d,c,o is_collinear
o, diff b,a,o // a,b by Th114;
then a,b // o, diff b,a,o by Th17;
then o, diff b,a,o // c,d by A2, A5, Def1;
then o, diff b,a,o // o, diff d,c,o by A6, A4, Th20;
hence o, diff b,a,o, diff d,c,o is_collinear by Def2; :: thesis: verum

end;

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;

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

end;

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

proof

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

A8: now

A9: o, diff d,c,o // c,d by Th114;
assume that
A10: o <> diff b,a,o and
A11: o <> diff d,c,o ; :: thesis: a,b // c,d
( o, diff b,a,o // o, diff d,c,o & o, diff b,a,o // a,b ) by A7, Def2, Th114;
then o, diff d,c,o // a,b by A10, Def1;
hence a,b // c,d by A11, A9, Def1; :: thesis: verum

end;

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;

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

end;

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