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