let SAS be Semi_Affine_Space; for p, q, r, s, o being Element of SAS st p,q // r,s holds
p,q // sum (p,r,o), sum (q,s,o)
let p, q, r, s, o be Element of SAS; ( p,q // r,s implies p,q // sum (p,r,o), sum (q,s,o) )
assume A1:
p,q // r,s
; p,q // sum (p,r,o), sum (q,s,o)
now consider t being
Element of
SAS such that A2:
congr o,
q,
r,
t
by Th82;
assume that A3:
p <> q
and A4:
r <> s
;
p,q // sum (p,r,o), sum (q,s,o)
congr o,
q,
s,
sum (
q,
s,
o)
by Def5;
then
congr r,
t,
s,
sum (
q,
s,
o)
by A2, Th85;
then A5:
congr r,
s,
t,
sum (
q,
s,
o)
by Th89;
then A6:
t <> sum (
q,
s,
o)
by A4, Th74;
r,
s // t,
sum (
q,
s,
o)
by A5, Th76;
then A7:
p,
q // t,
sum (
q,
s,
o)
by A1, A4, Th20;
congr o,
p,
r,
sum (
p,
r,
o)
by Def5;
then
congr p,
o,
sum (
p,
r,
o),
r
by Th89;
then
p,
q // sum (
p,
r,
o),
t
by A2, Th76, Th90;
then
p,
q // t,
sum (
p,
r,
o)
by Th17;
then
t,
sum (
q,
s,
o)
// t,
sum (
p,
r,
o)
by A3, A7, Def1;
then
t,
sum (
q,
s,
o)
// sum (
p,
r,
o),
sum (
q,
s,
o)
by Th18;
hence
p,
q // sum (
p,
r,
o),
sum (
q,
s,
o)
by A6, A7, Th20;
verum end;
hence
p,q // sum (p,r,o), sum (q,s,o)
by Th14, Th110; verum