let S be OAffinSpace; :: thesis: for AS being non empty AffinStruct st AS = Lambda S holds
( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )
let AS be non empty AffinStruct ; :: thesis: ( AS = Lambda S implies ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) ) )
assume A1:
AS = Lambda S
; :: thesis: ( ex x, y being Element of AS st x <> y & ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )
hence
ex x, y being Element of AS st x <> y
by STRUCT_0:def 10; :: thesis: ( ( for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) ) ) & not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )
thus
for x, y, z, t, u, w being Element of AS holds
( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) )
:: thesis: ( not for x, y, z being Element of AS holds x,y // x,z & ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )proof
let x,
y,
z,
t,
u,
w be
Element of
AS;
:: thesis: ( x,y // y,x & x,y // z,z & ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) )
reconsider x' =
x,
y' =
y,
z' =
z,
t' =
t,
u' =
u,
w' =
w as
Element of
S by A1;
(
x',
y' '||' y',
x' &
x',
y' '||' z',
z' )
by Th24, Th25;
hence
(
x,
y // y,
x &
x,
y // z,
z )
by A1, Th45;
:: thesis: ( ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) )
(
x' <> y' &
x',
y' '||' z',
t' &
x',
y' '||' u',
w' implies
z',
t' '||' u',
w' )
by Lm2;
hence
(
x <> y &
x,
y // z,
t &
x,
y // u,
w implies
z,
t // u,
w )
by A1, Th45;
:: thesis: ( x,y // x,z implies y,x // y,z )
(
x',
y' '||' x',
z' implies
y',
x' '||' y',
z' )
by Th26;
hence
(
x,
y // x,
z implies
y,
x // y,
z )
by A1, Th45;
:: thesis: verum
end;
thus
not for x, y, z being Element of AS holds x,y // x,z
:: thesis: ( ( for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t ) ) & ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )proof
consider x',
y',
z' being
Element of
S such that A2:
not
x',
y' '||' x',
z'
by Th29;
reconsider x =
x',
y =
y',
z =
z' as
Element of
AS by A1;
not
x,
y // x,
z
by A1, A2, Th45;
hence
not for
x,
y,
z being
Element of
AS holds
x,
y // x,
z
;
:: thesis: verum
end;
thus
for x, y, z being Element of AS ex t being Element of AS st
( x,z // y,t & y <> t )
:: thesis: ( ( for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t ) ) & ( for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u ) ) )proof
let x,
y,
z be
Element of
AS;
:: thesis: ex t being Element of AS st
( x,z // y,t & y <> t )
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
S by A1;
consider t' being
Element of
S such that A3:
(
x',
z' '||' y',
t' &
y' <> t' )
by Th30;
reconsider t =
t' as
Element of
AS by A1;
(
x,
z // y,
t &
y <> t )
by A1, A3, Th45;
hence
ex
t being
Element of
AS st
(
x,
z // y,
t &
y <> t )
;
:: thesis: verum
end;
thus
for x, y, z being Element of AS ex t being Element of AS st
( x,y // z,t & x,z // y,t )
:: thesis: for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u )proof
let x,
y,
z be
Element of
AS;
:: thesis: ex t being Element of AS st
( x,y // z,t & x,z // y,t )
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
S by A1;
consider t' being
Element of
S such that A4:
(
x',
y' '||' z',
t' &
x',
z' '||' y',
t' )
by Th31;
reconsider t =
t' as
Element of
AS by A1;
(
x,
y // z,
t &
x,
z // y,
t )
by A1, A4, Th45;
hence
ex
t being
Element of
AS st
(
x,
y // z,
t &
x,
z // y,
t )
;
:: thesis: verum
end;
thus
for x, y, z, t being Element of AS st z,x // x,t & x <> z holds
ex u being Element of AS st
( y,x // x,u & y,z // t,u )
:: thesis: verumproof
let x,
y,
z,
t be
Element of
AS;
:: thesis: ( z,x // x,t & x <> z implies ex u being Element of AS st
( y,x // x,u & y,z // t,u ) )
assume A5:
(
z,
x // x,
t &
x <> z )
;
:: thesis: ex u being Element of AS st
( y,x // x,u & y,z // t,u )
reconsider x' =
x,
y' =
y,
z' =
z,
t' =
t as
Element of
S by A1;
(
z',
x' '||' x',
t' &
x' <> z' )
by A1, A5, Th45;
then consider u' being
Element of
S such that A6:
(
y',
x' '||' x',
u' &
y',
z' '||' t',
u' )
by Th32;
reconsider u =
u' as
Element of
AS by A1;
(
y,
x // x,
u &
y,
z // t,
u )
by A1, A6, Th45;
hence
ex
u being
Element of
AS st
(
y,
x // x,
u &
y,
z // t,
u )
;
:: thesis: verum
end;