let X be OrtAfPl; :: thesis: ex a, b, c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
consider a, p being Element of X such that
A1: a <> p by ANALMETR:51;
consider b being Element of X such that
A2: ( a,p _|_ p,b & p <> b ) by ANALMETR:51;
consider c being Element of X such that
A3: ( p,c _|_ a,b & LIN a,b,c ) by ANALMETR:91;
take a ; :: thesis: ex b, c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
take b ; :: thesis: ex c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
take c ; :: thesis: ( LIN a,b,c & a <> b & b <> c & c <> a )
thus LIN a,b,c by A3; :: thesis: ( a <> b & b <> c & c <> a )
thus a <> b :: thesis: ( b <> c & c <> a )

proof

assume not a <> b ; :: thesis: contradiction
then a,p _|_ a,p by A2, ANALMETR:83;
hence contradiction by A1, ANALMETR:51; :: thesis: verum

end;

reconsider a' = a, b' = b, p' = p as Element of (Af X) by ANALMETR:47;
thus b <> c :: thesis: c <> a

proof

assume not b <> c ; :: thesis: contradiction
then a,p // a,b by A2, A3, ANALMETR:85;
then LIN a,p,b by ANALMETR:def 11;
then LIN a',p',b' by ANALMETR:55;
then LIN p',a',b' by AFF_1:15;
then LIN p,a,b by ANALMETR:55;
then p,a // p,b by ANALMETR:def 11;
then a,p _|_ p,a by A2, ANALMETR:84;
then a,p _|_ a,p by ANALMETR:83;
hence contradiction by A1, ANALMETR:51; :: thesis: verum

end;

assume not c <> a ; :: thesis: contradiction
then a,p _|_ a,b by A3, ANALMETR:83;
then p,b // a,b by A1, A2, ANALMETR:85;
then b,p // b,a by ANALMETR:81;
then LIN b,p,a by ANALMETR:def 11;
then LIN b',p',a' by ANALMETR:55;
then LIN p',a',b' by AFF_1:15;
then LIN p,a,b by ANALMETR:55;
then p,a // p,b by ANALMETR:def 11;
then a,p _|_ p,a by A2, ANALMETR:84;
then a,p _|_ a,p by ANALMETR:83;
hence contradiction by A1, ANALMETR:51; :: thesis: verum