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

( 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