let MS be OrtAfPl; :: thesis: ( MS is Euclidean iff MS is satisfying_3H )
A1: now :: thesis: ( MS is satisfying_3H implies MS is Euclidean )
assume A2: MS is satisfying_3H ; :: thesis: MS is Euclidean
now :: thesis: for a, b, c, d being Element of MS st a,b _|_ c,d & b,c _|_ a,d holds
b,d _|_ a,c
let a, b, c, d be Element of MS; :: thesis: ( 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 ; :: thesis: b,d _|_ a,c
A5: now :: thesis: ( 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 ; :: thesis: b,d _|_ a,c
then 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; :: thesis: verum
end;
now :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum
end;
hence b,d _|_ a,c by A5; :: thesis: verum
end;
hence MS is Euclidean ; :: thesis: verum
end;
now :: thesis: ( MS is Euclidean implies MS is satisfying_3H )
assume A14: MS is Euclidean ; :: thesis: MS is satisfying_3H
now :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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; :: thesis: verum
end;
hence MS is satisfying_3H by CONAFFM:def 3; :: thesis: verum
end;
hence ( MS is Euclidean iff MS is satisfying_3H ) by A1; :: thesis: verum