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 and
A3: p <> b by ANALMETR:51;
reconsider a9 = a, b9 = b, p9 = p as Element of (Af X) by ANALMETR:47;
consider c being Element of X such that
A4: p,c _|_ a,b and
A5: 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 A5; :: 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;

thus b <> c :: thesis: c <> a

proof

assume not b <> c ; :: thesis: contradiction
then a,p // a,b by A2, A3, A4, ANALMETR:85;
then LIN a,p,b by ANALMETR:def 11;
then LIN a9,p9,b9 by ANALMETR:55;
then LIN p9,a9,b9 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, A3, 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 A4, 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 b9,p9,a9 by ANALMETR:55;
then LIN p9,a9,b9 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, A3, ANALMETR:84;
then a,p _|_ a,p by ANALMETR:83;
hence contradiction by A1, ANALMETR:51; :: thesis: verum