let SAS be Semi_Affine_Space; :: thesis: 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; :: thesis: ( p,q // r,s implies p,q // sum p,r,o, sum q,s,o )
assume A1:
p,q // r,s
; :: thesis: p,q // sum p,r,o, sum q,s,o
now assume A2:
(
p <> q &
r <> s )
;
:: thesis: p,q // sum p,r,o, sum q,s,oconsider t being
Element of
SAS such that A3:
congr o,
q,
r,
t
by Th82;
(
congr o,
q,
r,
t &
congr o,
q,
s,
sum q,
s,
o )
by A3, Def5;
then
congr r,
t,
s,
sum q,
s,
o
by Th85;
then
congr r,
s,
t,
sum q,
s,
o
by Th89;
then
(
t <> sum q,
s,
o &
r,
s // t,
sum q,
s,
o )
by A2, Th74, Th76;
then A4:
(
t <> sum q,
s,
o &
p,
q // t,
sum q,
s,
o )
by A1, A2, Th20;
congr o,
p,
r,
sum p,
r,
o
by Def5;
then
(
congr p,
o,
sum p,
r,
o,
r &
congr o,
q,
r,
t )
by A3, Th89;
then
p,
q // sum p,
r,
o,
t
by Th76, Th90;
then
p,
q // t,
sum p,
r,
o
by Th17;
then
t,
sum q,
s,
o // t,
sum p,
r,
o
by A2, A4, 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 A4, Th20;
:: thesis: verum end;
hence
p,q // sum p,r,o, sum q,s,o
by Th14, Th110; :: thesis: verum