let S be OAffinSpace; for z, x, t, y being Element of S st z,x '||' x,t & x <> z holds
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
let z, x, t, y be Element of S; ( z,x '||' x,t & x <> z implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )
assume that
A1:
z,x '||' x,t
and
A2:
x <> z
; ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
A3:
now consider p being
Element of
S such that A4:
Mid z,
x,
p
and A5:
x <> p
by Th17;
A6:
z,
x // x,
p
by A4, Def3;
then consider q being
Element of
S such that A7:
y,
x // x,
q
and A8:
y,
z // p,
q
by A2, ANALOAF:def 5;
assume A9:
z,
x // t,
x
;
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )then
x,
p // t,
x
by A2, A6, ANALOAF:def 5;
then
p,
x // x,
t
by Th5;
then consider r being
Element of
S such that A10:
q,
x // x,
r
and A11:
q,
p // t,
r
by A5, ANALOAF:def 5;
A12:
now assume
q = p
;
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )then A13:
x,
p // y,
x
by A7, Th5;
x,
p // z,
x
by A6, Th5;
then
z,
x // y,
x
by A5, A13, ANALOAF:def 5;
then
y,
x // t,
x
by A2, A9, ANALOAF:def 5;
then A14:
y,
x '||' x,
t
by Def4;
y,
z // t,
t
by ANALOAF:def 5;
then
y,
z '||' t,
t
by Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A14;
verum end; A15:
now A16:
x,
z // x,
t
by A9, Th5;
assume A17:
q = x
;
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
p,
x // x,
z
by A6, Th5;
then
y,
z // x,
z
by A5, A8, A17, Th6;
then
y,
z // x,
t
by A2, A16, Th6;
then A18:
y,
z '||' t,
x
by Def4;
y,
x // x,
x
by Th7;
then
y,
x '||' x,
x
by Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A18;
verum end; now assume that A19:
q <> p
and A20:
q <> x
;
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
x,
q // r,
x
by A10, Th5;
then
y,
x // r,
x
by A7, A20, Th6;
then A21:
y,
x '||' x,
r
by Def4;
p,
q // r,
t
by A11, Th5;
then
y,
z // r,
t
by A8, A19, Th6;
then
y,
z '||' t,
r
by Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A21;
verum end; hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A12, A15;
verum end;
now assume
z,
x // x,
t
;
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )then consider u being
Element of
S such that A22:
(
y,
x // x,
u &
y,
z // t,
u )
by A2, ANALOAF:def 5;
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A22, Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
;
verum end;
hence
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
by A1, A3, Def4; verum