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:39;
consider b being Element of X such that
A2: a,p _|_ p,b and
A3: p <> b by ANALMETR:39;
reconsider a9 = a, b9 = b, p9 = p as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
consider c being Element of X such that
A4: p,c _|_ a,b and
A5: LIN a,b,c by ANALMETR:69;
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:61;
hence contradiction by A1, ANALMETR:39; :: 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:63;
then LIN a,p,b by ANALMETR:def 10;
then LIN a9,p9,b9 by ANALMETR:40;
then LIN p9,a9,b9 by AFF_1:6;
then LIN p,a,b by ANALMETR:40;
then p,a // p,b by ANALMETR:def 10;
then a,p _|_ p,a by A2, A3, ANALMETR:62;
then a,p _|_ a,p by ANALMETR:61;
hence contradiction by A1, ANALMETR:39; :: thesis: verum
end;
assume not c <> a ; :: thesis: contradiction
then a,p _|_ a,b by A4, ANALMETR:61;
then p,b // a,b by A1, A2, ANALMETR:63;
then b,p // b,a by ANALMETR:59;
then LIN b,p,a by ANALMETR:def 10;
then LIN b9,p9,a9 by ANALMETR:40;
then LIN p9,a9,b9 by AFF_1:6;
then LIN p,a,b by ANALMETR:40;
then p,a // p,b by ANALMETR:def 10;
then a,p _|_ p,a by A2, A3, ANALMETR:62;
then a,p _|_ a,p by ANALMETR:61;
hence contradiction by A1, ANALMETR:39; :: thesis: verum