let S be OAffinSpace; for x, y, z, t 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 x, y, z, t 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 ( z,x // t,x implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )consider p being
Element of
S such that A4:
Mid z,
x,
p
and A5:
x <> p
by Th13;
A6:
z,
x // x,
p
by A4;
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 Th2;
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 ( q = p implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )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, Th2;
x,
p // z,
x
by A6, Th2;
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
;
y,
z // t,
t
by ANALOAF:def 5;
then
y,
z '||' t,
t
;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A14;
verum end; A15:
now ( q = x implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )A16:
x,
z // x,
t
by A9, Th2;
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, Th2;
then
y,
z // x,
z
by A5, A8, A17, Th3;
then
y,
z // x,
t
by A2, A16, Th3;
then A18:
y,
z '||' t,
x
;
y,
x // x,
x
by Th4;
then
y,
x '||' x,
x
;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A18;
verum end; now ( q <> p & q <> x implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )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, Th2;
then
y,
x // r,
x
by A7, A20, Th3;
then A21:
y,
x '||' x,
r
;
p,
q // r,
t
by A11, Th2;
then
y,
z // r,
t
by A8, A19, Th3;
then
y,
z '||' t,
r
;
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 ( z,x // x,t implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )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;
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; verum