let MS be OrtAfPl; ( MS is Euclidean iff MS is satisfying_3H )
A1:
now ( MS is satisfying_3H implies MS is Euclidean )assume A2:
MS is
satisfying_3H
;
MS is Euclidean now for a, b, c, d being Element of MS st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,clet a,
b,
c,
d be
Element of
MS;
( a,b _|_ c,d & b,c _|_ a,d implies b,d _|_ a,c )assume that A3:
a,
b _|_ c,
d
and A4:
b,
c _|_ a,
d
;
b,d _|_ a,cA5:
now ( not LIN a,b,c implies b,d _|_ a,c )A6:
(
d,
a _|_ c,
b &
d,
c _|_ a,
b )
by A3, A4, ANALMETR:61;
assume A7:
not
LIN a,
b,
c
;
b,d _|_ a,cthen consider d1 being
Element of
MS such that A8:
d1,
a _|_ b,
c
and A9:
(
d1,
b _|_ a,
c &
d1,
c _|_ a,
b )
by A2, CONAFFM:def 3;
A10:
not
LIN a,
c,
b
by A7, Th4;
d1,
a _|_ c,
b
by A8, ANALMETR:61;
then
d,
b _|_ a,
c
by A9, A6, A10, Th6;
hence
b,
d _|_ a,
c
by ANALMETR:61;
verum end; now ( LIN a,b,c implies b,d _|_ a,c )A11:
(
a = c implies
b,
d _|_ a,
c )
by ANALMETR:58;
A12:
(
b = c implies
b,
d _|_ a,
c )
by A3, ANALMETR:61;
assume A13:
LIN a,
b,
c
;
b,d _|_ a,c
(
a = b implies
b,
d _|_ a,
c )
by A4, ANALMETR:61;
hence
b,
d _|_ a,
c
by A3, A4, A13, A11, A12, Th7;
verum end; hence
b,
d _|_ a,
c
by A5;
verum end; hence
MS is
Euclidean
;
verum end;
now ( MS is Euclidean implies MS is satisfying_3H )assume A14:
MS is
Euclidean
;
MS is satisfying_3H now for a, b, c being Element of MS st not LIN a,b,c holds
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )let a,
b,
c be
Element of
MS;
( not LIN a,b,c implies ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) )assume
not
LIN a,
b,
c
;
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )then consider d being
Element of
MS such that A15:
(
d,
a _|_ b,
c &
d,
b _|_ a,
c )
by Th5;
take d =
d;
( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b )
(
b,
c _|_ a,
d &
c,
a _|_ b,
d )
by A15, ANALMETR:61;
then
c,
d _|_ b,
a
by A14;
hence
(
d,
a _|_ b,
c &
d,
b _|_ a,
c &
d,
c _|_ a,
b )
by A15, ANALMETR:61;
verum end; hence
MS is
satisfying_3H
by CONAFFM:def 3;
verum end;
hence
( MS is Euclidean iff MS is satisfying_3H )
by A1; verum