theorem
for
AS being non
empty AffinStruct holds
(
AS is
AffinPlane iff ( 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 ) ) & ( for
x,
y,
z,
t being
Element of
AS st not
x,
y // z,
t holds
ex
u being
Element of
AS st
(
x,
y // x,
u &
z,
t // z,
u ) ) ) )
by Def6, Def7, STRUCT_0:def 10;