let POS be non empty ParOrtStr ; ( POS is OrtAfPl-like iff ( ex a, b being Element of POS st a <> b & ( for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) ) )
set P = AffinStruct(# the carrier of POS, the CONGR of POS #);
hereby ( ex a, b being Element of POS st a <> b & ( for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) implies POS is OrtAfPl-like )
assume A1:
POS is
OrtAfPl-like
;
( ex x, y being Element of POS st x <> y & ( for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) ) ) )then
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) is
AffinPlane
;
hence
ex
x,
y being
Element of
POS st
x <> y
by DIRAF:46;
for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )let a,
b,
c,
d,
p,
q,
r,
s be
Element of
POS;
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )reconsider a9 =
a,
b9 =
b,
c9 =
c,
d9 =
d,
p9 =
p,
q9 =
q,
r9 =
r,
s9 =
s as
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) ;
consider x9 being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #)
such that A2:
(
a9,
b9 // c9,
x9 &
a9,
c9 // b9,
x9 )
by A1, DIRAF:46;
(
a9,
b9 // b9,
a9 &
a9,
b9 // c9,
c9 )
by A1, DIRAF:46;
hence
(
a,
b // b,
a &
a,
b // c,
c )
by Th36;
( ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )hereby ( ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
assume
(
a,
b // p,
q &
a,
b // r,
s )
;
( p,q // r,s or a = b )then
(
a9,
b9 // p9,
q9 &
a9,
b9 // r9,
s9 )
by Th36;
then
(
p9,
q9 // r9,
s9 or
a9 = b9 )
by A1, DIRAF:46;
hence
(
p,
q // r,
s or
a = b )
by Th36;
verum
end; hereby ( ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
assume
a,
b // a,
c
;
b,a // b,cthen
a9,
b9 // a9,
c9
by Th36;
then
b9,
a9 // b9,
c9
by A1, DIRAF:46;
hence
b,
a // b,
c
by Th36;
verum
end; reconsider x =
x9 as
Element of
POS ;
consider x9,
y9,
z9 being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #)
such that A3:
not
x9,
y9 // x9,
z9
by A1, DIRAF:46;
(
a,
b // c,
x &
a,
c // b,
x )
by A2, Th36;
hence
ex
x being
Element of
POS st
(
a,
b // c,
x &
a,
c // b,
x )
;
( not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )reconsider x =
x9,
y =
y9,
z =
z9 as
Element of
POS ;
consider x9 being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #)
such that A4:
a9,
b9 // c9,
x9
and A5:
c9 <> x9
by A1, DIRAF:46;
not
x,
y // x,
z
by A3, Th36;
hence
not for
x,
y,
z being
Element of
POS holds
x,
y // x,
z
;
( ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )reconsider x =
x9 as
Element of
POS ;
a,
b // c,
x
by A4, Th36;
hence
ex
x being
Element of
POS st
(
a,
b // c,
x &
c <> x )
by A5;
( ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )hereby ( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
assume that A6:
a,
b // b,
d
and A7:
b <> a
;
ex x being Element of POS st
( c,b // b,x & c,a // d,x )
a9,
b9 // b9,
d9
by A6, Th36;
then consider x9 being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #)
such that A8:
(
c9,
b9 // b9,
x9 &
c9,
a9 // d9,
x9 )
by A1, A7, DIRAF:46;
reconsider x =
x9 as
Element of
POS ;
(
c,
b // b,
x &
c,
a // d,
x )
by A8, Th36;
hence
ex
x being
Element of
POS st
(
c,
b // b,
x &
c,
a // d,
x )
;
verum
end; thus
( (
a,
b _|_ a,
b implies
a = b ) &
a,
b _|_ c,
c & (
a,
b _|_ c,
d implies (
a,
b _|_ d,
c &
c,
d _|_ a,
b ) ) & (
a,
b _|_ p,
q &
a,
b // r,
s & not
p,
q _|_ r,
s implies
a = b ) & (
a,
b _|_ p,
q &
a,
b _|_ r,
s & not
p,
q // r,
s implies
a = b ) & ex
x being
Element of
POS st
(
a,
b _|_ c,
x &
c <> x ) )
by A1;
( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) )assume
not
a,
b // c,
d
;
ex x being Element of POS st
( a,b // a,x & c,d // c,x )then
not
a9,
b9 // c9,
d9
by Th36;
then consider x9 being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #)
such that A9:
(
a9,
b9 // a9,
x9 &
c9,
d9 // c9,
x9 )
by A1, DIRAF:46;
reconsider x =
x9 as
Element of
POS ;
(
a,
b // a,
x &
c,
d // c,
x )
by A9, Th36;
hence
ex
x being
Element of
POS st
(
a,
b // a,
x &
c,
d // c,
x )
;
verum
end;
given a, b being Element of POS such that A10:
a <> b
; ( ex a, b, c, d, p, q, r, s being Element of POS st
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) implies ( not a,b // c,d & ( for x being Element of POS holds
( not a,b // a,x or not c,d // c,x ) ) ) ) or POS is OrtAfPl-like )
assume A11:
for a, b, c, d, p, q, r, s being Element of POS holds
( a,b // b,a & a,b // c,c & ( a,b // p,q & a,b // r,s & not p,q // r,s implies a = b ) & ( a,b // a,c implies b,a // b,c ) & ex x being Element of POS st
( a,b // c,x & a,c // b,x ) & not for x, y, z being Element of POS holds x,y // x,z & ex x being Element of POS st
( a,b // c,x & c <> x ) & ( a,b // b,d & b <> a implies ex x being Element of POS st
( c,b // b,x & c,a // d,x ) ) & ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) & ex x being Element of POS st
( a,b _|_ c,x & c <> x ) & ( not a,b // c,d implies ex x being Element of POS st
( a,b // a,x & c,d // c,x ) ) )
; POS is OrtAfPl-like
A12:
now for x, y, z being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ex t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,z // y,t & y <> t )let x,
y,
z be
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #);
ex t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,z // y,t & y <> t )reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
POS ;
consider t9 being
Element of
POS such that A13:
x9,
z9 // y9,
t9
and A14:
y9 <> t9
by A11;
reconsider t =
t9 as
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) ;
x,
z // y,
t
by A13, Th36;
hence
ex
t being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) st
(
x,
z // y,
t &
y <> t )
by A14;
verum end;
A15:
now for x, y, z, t, u, w being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) 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 ) )let x,
y,
z,
t,
u,
w be
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #);
( 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 a =
x,
b =
y,
c =
z,
d =
t,
e =
u,
f =
w as
Element of
POS ;
(
a,
b // b,
a &
a,
b // c,
c )
by A11;
hence
(
x,
y // y,
x &
x,
y // z,
z )
by Th36;
( ( x <> y & x,y // z,t & x,y // u,w implies z,t // u,w ) & ( x,y // x,z implies y,x // y,z ) )thus
(
x <> y &
x,
y // z,
t &
x,
y // u,
w implies
z,
t // u,
w )
( x,y // x,z implies y,x // y,z )proof
assume that A16:
x <> y
and A17:
(
x,
y // z,
t &
x,
y // u,
w )
;
z,t // u,w
(
a,
b // c,
d &
a,
b // e,
f )
by A17, Th36;
then
c,
d // e,
f
by A11, A16;
hence
z,
t // u,
w
by Th36;
verum
end; thus
(
x,
y // x,
z implies
y,
x // y,
z )
verumproof
assume
x,
y // x,
z
;
y,x // y,z
then
a,
b // a,
c
by Th36;
then
b,
a // b,
c
by A11;
hence
y,
x // y,
z
by Th36;
verum
end; end;
A18:
now for x, y, z, t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st not x,y // z,t holds
ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,y // x,u & z,t // z,u )let x,
y,
z,
t be
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #);
( not x,y // z,t implies ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,y // x,u & z,t // z,u ) )assume A19:
not
x,
y // z,
t
;
ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,y // x,u & z,t // z,u )reconsider x9 =
x,
y9 =
y,
z9 =
z,
t9 =
t as
Element of
POS ;
not
x9,
y9 // z9,
t9
by A19, Th36;
then consider u9 being
Element of
POS such that A20:
(
x9,
y9 // x9,
u9 &
z9,
t9 // z9,
u9 )
by A11;
reconsider u =
u9 as
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) ;
(
x,
y // x,
u &
z,
t // z,
u )
by A20, Th36;
hence
ex
u being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) st
(
x,
y // x,
u &
z,
t // z,
u )
;
verum end;
A21:
now for x, y, z, t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st z,x // x,t & x <> z holds
ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( y,x // x,u & y,z // t,u )let x,
y,
z,
t be
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #);
( z,x // x,t & x <> z implies ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( y,x // x,u & y,z // t,u ) )assume that A22:
z,
x // x,
t
and A23:
x <> z
;
ex u being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( y,x // x,u & y,z // t,u )reconsider x9 =
x,
y9 =
y,
z9 =
z,
t9 =
t as
Element of
POS ;
z9,
x9 // x9,
t9
by A22, Th36;
then consider u9 being
Element of
POS such that A24:
(
y9,
x9 // x9,
u9 &
y9,
z9 // t9,
u9 )
by A11, A23;
reconsider u =
u9 as
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) ;
(
y,
x // x,
u &
y,
z // t,
u )
by A24, Th36;
hence
ex
u being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) st
(
y,
x // x,
u &
y,
z // t,
u )
;
verum end;
A25:
now for x, y, z being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ex t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,y // z,t & x,z // y,t )let x,
y,
z be
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #);
ex t being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) st
( x,y // z,t & x,z // y,t )reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
POS ;
consider t9 being
Element of
POS such that A26:
(
x9,
y9 // z9,
t9 &
x9,
z9 // y9,
t9 )
by A11;
reconsider t =
t9 as
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) ;
(
x,
y // z,
t &
x,
z // y,
t )
by A26, Th36;
hence
ex
t being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) st
(
x,
y // z,
t &
x,
z // y,
t )
;
verum end;
not for x, y, z being Element of AffinStruct(# the carrier of POS, the CONGR of POS #) holds x,y // x,z
proof
consider x,
y,
z being
Element of
POS such that A27:
not
x,
y // x,
z
by A11;
reconsider x9 =
x,
y9 =
y,
z9 =
z as
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) ;
not
x9,
y9 // x9,
z9
by A27, Th36;
hence
not for
x,
y,
z being
Element of
AffinStruct(# the
carrier of
POS, the
CONGR of
POS #) holds
x,
y // x,
z
;
verum
end;
hence
AffinStruct(# the carrier of POS, the CONGR of POS #) is AffinPlane
by A10, A15, A12, A25, A21, A18, DIRAF:46; ANALMETR:def 9 ( ( for a, b, c, d, p, q, r, s being Element of POS holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) ) ) & ( for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x ) ) )
thus
for a, b, c, d, p, q, r, s being Element of POS holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b ) )
by A11; for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x )
thus
for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x )
by A11; verum