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