let POS be OrtAfSp; :: thesis: ( Af POS is AffinPlane implies POS is OrtAfPl )
assume A1:
Af POS is AffinPlane
; :: thesis: POS is OrtAfPl
A2:
now let a,
b,
c,
d,
p,
q,
r,
s be
Element of
POS;
:: thesis: ( ( 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 ) )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 ) )
by Def9;
:: thesis: ( a,b _|_ p,q & a,b _|_ r,s & not p,q // r,s implies a = b )thus
(
a,
b _|_ p,
q &
a,
b _|_ r,
s & not
p,
q // r,
s implies
a = b )
:: thesis: verumproof
reconsider a' =
a,
b' =
b,
p' =
p,
q' =
q,
r' =
r,
s' =
s as
Element of
(Af POS) ;
assume that A3:
a,
b _|_ p,
q
and A4:
a,
b _|_ r,
s
;
:: thesis: ( p,q // r,s or a = b )
A5:
p,
q _|_ a,
b
by A3, Def9;
A6:
r,
s _|_ a,
b
by A4, Def9;
assume A7:
( not
p,
q // r,
s & not
a = b )
;
:: thesis: contradiction
then A8:
not
p',
q' // r',
s'
by Th48;
then A9:
p' <> q'
by AFF_1:12;
consider x' being
Element of
(Af POS) such that A10:
LIN p',
q',
x'
and A11:
LIN r',
s',
x'
by A1, A8, AFF_1:74;
reconsider x =
x' as
Element of
POS ;
A12:
r' <> s'
by A8, AFF_1:12;
LIN s',
r',
x'
by A11, AFF_1:15;
then
s',
r' // s',
x'
by AFF_1:def 1;
then A13:
r',
s' // x',
s'
by AFF_1:13;
then
r,
s // x,
s
by Th48;
then
a,
b _|_ x,
s
by A12, A6, Def9;
then A14:
x,
s _|_ a,
b
by Def9;
LIN q',
p',
x'
by A10, AFF_1:15;
then
q',
p' // q',
x'
by AFF_1:def 1;
then
p',
q' // x',
q'
by AFF_1:13;
then
p,
q // x,
q
by Th48;
then A15:
a,
b _|_ x,
q
by A9, A5, Def9;
A16:
now consider y' being
Element of
(Af POS) such that A17:
(
a',
b' // q',
y' &
q' <> y' )
by DIRAF:47;
assume that A18:
x <> q
and A19:
x <> s
;
:: thesis: contradiction
not
q',
y' // x',
s'
proof
assume
q',
y' // x',
s'
;
:: thesis: contradiction
then
q',
y' // r',
s'
by A13, A19, AFF_1:14;
then
r',
s' // a',
b'
by A17, AFF_1:14;
then
r,
s // a,
b
by Th48;
then
a,
b _|_ a,
b
by A12, A6, Def9;
hence
contradiction
by A7, Def9;
:: thesis: verum
end; then consider z' being
Element of
(Af POS) such that A20:
LIN q',
y',
z'
and A21:
LIN x',
s',
z'
by A1, AFF_1:74;
reconsider z =
z' as
Element of
POS ;
q',
y' // q',
z'
by A20, AFF_1:def 1;
then
a',
b' // q',
z'
by A17, AFF_1:14;
then A22:
a,
b // q,
z
by Th48;
A23:
x',
s' // x',
z'
by A21, AFF_1:def 1;
then
x,
s // x,
z
by Th48;
then
a,
b _|_ x,
z
by A14, A19, Def9;
then
a,
b _|_ q,
z
by A15, Def9;
then
q,
z _|_ q,
z
by A7, A22, Def9;
then
x',
s' // x',
q'
by A23, Def9;
then A24:
LIN x',
s',
q'
by AFF_1:def 1;
(
LIN x',
s',
x' &
LIN x',
q',
p' )
by A10, AFF_1:15, AFF_1:16;
then
LIN x',
s',
p'
by A18, A24, AFF_1:20;
then
x',
s' // p',
q'
by A24, AFF_1:19;
then
p',
q' // r',
s'
by A13, A19, AFF_1:14;
hence
contradiction
by A7, Th48;
:: thesis: verum end;
r',
s' // r',
x'
by A11, AFF_1:def 1;
then A25:
r',
s' // x',
r'
by AFF_1:13;
then
r,
s // x,
r
by Th48;
then
a,
b _|_ x,
r
by A12, A6, Def9;
then A26:
x,
r _|_ a,
b
by Def9;
A27:
now consider y' being
Element of
(Af POS) such that A28:
(
a',
b' // q',
y' &
q' <> y' )
by DIRAF:47;
assume that A29:
x <> q
and A30:
x <> r
;
:: thesis: contradiction
not
q',
y' // x',
r'
proof
assume
q',
y' // x',
r'
;
:: thesis: contradiction
then
q',
y' // r',
s'
by A25, A30, AFF_1:14;
then
r',
s' // a',
b'
by A28, AFF_1:14;
then
r,
s // a,
b
by Th48;
then
a,
b _|_ a,
b
by A12, A6, Def9;
hence
contradiction
by A7, Def9;
:: thesis: verum
end; then consider z' being
Element of
(Af POS) such that A31:
LIN q',
y',
z'
and A32:
LIN x',
r',
z'
by A1, AFF_1:74;
reconsider z =
z' as
Element of
POS ;
q',
y' // q',
z'
by A31, AFF_1:def 1;
then
a',
b' // q',
z'
by A28, AFF_1:14;
then A33:
a,
b // q,
z
by Th48;
A34:
x',
r' // x',
z'
by A32, AFF_1:def 1;
then
x,
r // x,
z
by Th48;
then
a,
b _|_ x,
z
by A26, A30, Def9;
then
a,
b _|_ q,
z
by A15, Def9;
then
q,
z _|_ q,
z
by A7, A33, Def9;
then
x',
r' // x',
q'
by A34, Def9;
then A35:
LIN x',
r',
q'
by AFF_1:def 1;
(
LIN x',
r',
x' &
LIN x',
q',
p' )
by A10, AFF_1:15, AFF_1:16;
then
LIN x',
r',
p'
by A29, A35, AFF_1:20;
then
x',
r' // p',
q'
by A35, AFF_1:19;
then
p',
q' // r',
s'
by A25, A30, AFF_1:14;
hence
contradiction
by A7, Th48;
:: thesis: verum end;
p',
q' // p',
x'
by A10, AFF_1:def 1;
then
p',
q' // x',
p'
by AFF_1:13;
then
p,
q // x,
p
by Th48;
then A36:
a,
b _|_ x,
p
by A9, A5, Def9;
A37:
now consider y' being
Element of
(Af POS) such that A38:
(
a',
b' // p',
y' &
p' <> y' )
by DIRAF:47;
assume that A39:
x <> p
and A40:
x <> s
;
:: thesis: contradiction
not
p',
y' // x',
s'
proof
assume
p',
y' // x',
s'
;
:: thesis: contradiction
then
p',
y' // r',
s'
by A13, A40, AFF_1:14;
then
r',
s' // a',
b'
by A38, AFF_1:14;
then
r,
s // a,
b
by Th48;
then
a,
b _|_ a,
b
by A12, A6, Def9;
hence
contradiction
by A7, Def9;
:: thesis: verum
end; then consider z' being
Element of
(Af POS) such that A41:
LIN p',
y',
z'
and A42:
LIN x',
s',
z'
by A1, AFF_1:74;
reconsider z =
z' as
Element of
POS ;
p',
y' // p',
z'
by A41, AFF_1:def 1;
then
a',
b' // p',
z'
by A38, AFF_1:14;
then A43:
a,
b // p,
z
by Th48;
A44:
x',
s' // x',
z'
by A42, AFF_1:def 1;
then
x,
s // x,
z
by Th48;
then
a,
b _|_ x,
z
by A14, A40, Def9;
then
a,
b _|_ p,
z
by A36, Def9;
then
p,
z _|_ p,
z
by A7, A43, Def9;
then
x',
s' // x',
p'
by A44, Def9;
then A45:
LIN x',
s',
p'
by AFF_1:def 1;
(
LIN x',
s',
x' &
LIN x',
p',
q' )
by A10, AFF_1:15, AFF_1:16;
then
LIN x',
s',
q'
by A39, A45, AFF_1:20;
then
x',
s' // p',
q'
by A45, AFF_1:19;
then
p',
q' // r',
s'
by A13, A40, AFF_1:14;
hence
contradiction
by A7, Th48;
:: thesis: verum end;
now consider y' being
Element of
(Af POS) such that A46:
(
a',
b' // p',
y' &
p' <> y' )
by DIRAF:47;
assume that A47:
x <> p
and A48:
x <> r
;
:: thesis: contradiction
not
p',
y' // x',
r'
proof
assume
p',
y' // x',
r'
;
:: thesis: contradiction
then
p',
y' // r',
s'
by A25, A48, AFF_1:14;
then
r',
s' // a',
b'
by A46, AFF_1:14;
then
r,
s // a,
b
by Th48;
then
a,
b _|_ a,
b
by A12, A6, Def9;
hence
contradiction
by A7, Def9;
:: thesis: verum
end; then consider z' being
Element of
(Af POS) such that A49:
LIN p',
y',
z'
and A50:
LIN x',
r',
z'
by A1, AFF_1:74;
reconsider z =
z' as
Element of
POS ;
p',
y' // p',
z'
by A49, AFF_1:def 1;
then
a',
b' // p',
z'
by A46, AFF_1:14;
then A51:
a,
b // p,
z
by Th48;
A52:
x',
r' // x',
z'
by A50, AFF_1:def 1;
then
x,
r // x,
z
by Th48;
then
a,
b _|_ x,
z
by A26, A48, Def9;
then
a,
b _|_ p,
z
by A36, Def9;
then
p,
z _|_ p,
z
by A7, A51, Def9;
then
x',
r' // x',
p'
by A52, Def9;
then A53:
LIN x',
r',
p'
by AFF_1:def 1;
(
LIN x',
r',
x' &
LIN x',
p',
q' )
by A10, AFF_1:15, AFF_1:16;
then
LIN x',
r',
q'
by A47, A53, AFF_1:20;
then
x',
r' // p',
q'
by A53, AFF_1:19;
then
p',
q' // r',
s'
by A25, A48, AFF_1:14;
hence
contradiction
by A7, Th48;
:: thesis: verum end;
hence
contradiction
by A8, A37, A27, A16, AFF_1:12;
:: thesis: verum
end; end;
for a, b, c being Element of POS ex x being Element of POS st
( a,b _|_ c,x & c <> x )
by Def9;
hence
POS is OrtAfPl
by A1, A2, Def10; :: thesis: verum