let X be OrtAfPl; :: thesis: for a, b being Element of X ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )
let a, b be Element of X; :: thesis: ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )
consider p, q, r being Element of X such that
A1: LIN p,q,r and
A2: p <> q and
A3: q <> r and
A4: r <> p by Th1;
reconsider a9 = a, b9 = b, p9 = p, q9 = q, r9 = r as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
LIN p9,q9,r9 by A1, ANALMETR:40;
then consider c9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A5: LIN a9,b9,c9 and
A6: a9 <> c9 and
A7: b9 <> c9 by A2, A3, A4, TRANSLAC:1;
reconsider c = c9 as Element of X ;
LIN a,b,c by A5, ANALMETR:40;
hence ex c being Element of X st
( LIN a,b,c & a <> c & b <> c ) by A6, A7; :: thesis: verum