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 )

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

( 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

thus
b <> c
:: thesis: c <> a
assume
not a <> b
; :: thesis: contradiction

then a,p _|_ a,p by A2, ANALMETR:61;

hence contradiction by A1, ANALMETR:39; :: thesis: verum

end;then a,p _|_ a,p by A2, ANALMETR:61;

hence contradiction by A1, ANALMETR:39; :: thesis: verum

proof

assume
not c <> a
; :: thesis: contradiction
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;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

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