let MS be OrtAfPl; :: thesis: ( MS is Euclidean iff MS is satisfying_3H )

A1: now

assume A2: MS is satisfying_3H ; :: thesis: MS is Euclidean

now

let a, b, c, d be Element of MS; :: thesis: ( a,b _|_ c,d & b,c _|_ a,d implies b,d _|_ a,c )
assume A3: ( a,b _|_ c,d & b,c _|_ a,d ) ; :: thesis: b,d _|_ a,c

A4: now

assume A5: not LIN a,b,c ; :: thesis: b,d _|_ a,c
then consider d1 being Element of MS such that
A6: ( d1,a _|_ b,c & d1,b _|_ a,c & d1,c _|_ a,b ) by A2, CONAFFM:def 3;
A7: ( d,a _|_ c,b & d,c _|_ a,b ) by A3, ANALMETR:83;
A8: ( d1,a _|_ c,b & d1,c _|_ a,b ) by A6, ANALMETR:83;
not LIN a,c,b by A5, Th4;
then d,b _|_ a,c by A6, A7, A8, Th6;
hence b,d _|_ a,c by ANALMETR:83; :: thesis: verum

end;

now

assume A9: LIN a,b,c ; :: thesis: b,d _|_ a,c
A10: ( a = c implies b,d _|_ a,c ) by ANALMETR:80;
A11: ( a = b implies b,d _|_ a,c ) by A3, ANALMETR:83;
( b = c implies b,d _|_ a,c ) by A3, ANALMETR:83;
hence b,d _|_ a,c by A3, A9, A10, A11, Th7; :: thesis: verum

end;

hence b,d _|_ a,c by A4; :: thesis: verum

end;

hence MS is Euclidean by Def1; :: thesis: verum

end;

now

assume A12: MS is Euclidean ; :: thesis: MS is satisfying_3H

now

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
A13: ( 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 A13, ANALMETR:83;
then c,d _|_ b,a by A12, Def1;
hence ( d,a _|_ b,c & d,b _|_ a,c & d,c _|_ a,b ) by A13, ANALMETR:83; :: 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