let S be OAffinSpace; :: thesis: 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; :: thesis: ( z,x '||' x,t & x <> z implies ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u ) )
assume A1:
( z,x '||' x,t & x <> z )
; :: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
A2:
now assume
z,
x // x,
t
;
:: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )then consider u being
Element of
S such that A3:
(
y,
x // x,
u &
y,
z // t,
u )
by A1, ANALOAF:def 5;
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A3, Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
;
:: thesis: verum end;
now assume A4:
z,
x // t,
x
;
:: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )consider p being
Element of
S such that A5:
(
Mid z,
x,
p &
x <> p )
by Th17;
A6:
z,
x // x,
p
by A5, Def3;
then consider q being
Element of
S such that A7:
(
y,
x // x,
q &
y,
z // p,
q )
by A1, ANALOAF:def 5;
x,
p // t,
x
by A1, A4, A6, ANALOAF:def 5;
then
p,
x // x,
t
by Th5;
then consider r being
Element of
S such that A8:
(
q,
x // x,
r &
q,
p // t,
r )
by A5, ANALOAF:def 5;
A9:
now assume
q = p
;
:: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )then
(
x,
p // z,
x &
x,
p // y,
x )
by A6, A7, Th5;
then
z,
x // y,
x
by A5, ANALOAF:def 5;
then
(
y,
x // t,
x &
y,
z // t,
t )
by A1, A4, ANALOAF:def 5;
then
(
y,
x '||' x,
t &
y,
z '||' t,
t )
by Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
;
:: thesis: verum end; A10:
now assume
q = x
;
:: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )then
(
y,
z // p,
x &
p,
x // x,
z )
by A6, A7, Th5;
then
(
y,
z // x,
z &
x,
z // x,
t )
by A4, A5, Th5, Th6;
then
(
y,
z // x,
t &
y,
x // x,
x )
by A1, Th6, Th7;
then
(
y,
z '||' t,
x &
y,
x '||' x,
x )
by Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
;
:: thesis: verum end; now assume A11:
(
q <> p &
q <> x )
;
:: thesis: ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
(
p,
q // y,
z &
p,
q // r,
t &
x,
q // r,
x )
by A7, A8, Th5;
then
(
y,
z // r,
t &
y,
x // r,
x )
by A7, A11, Th6;
then
(
y,
z '||' t,
r &
y,
x '||' x,
r )
by Def4;
hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
;
:: thesis: verum end; hence
ex
u being
Element of
S st
(
y,
x '||' x,
u &
y,
z '||' t,
u )
by A9, A10;
:: thesis: verum end;
hence
ex u being Element of S st
( y,x '||' x,u & y,z '||' t,u )
by A1, A2, Def4; :: thesis: verum