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 a' = a, b' = b, p' = p, q' = q, r' = r as Element of (Af X) by ANALMETR:47;
LIN p',q',r' by A1, ANALMETR:55;
then consider c' being Element of (Af X) such that
A5: LIN a',b',c' and
A6: a' <> c' and
A7: b' <> c' by A2, A3, A4, TRANSLAC:2;
reconsider c = c' as Element of X by ANALMETR:47;
LIN a,b,c by A5, ANALMETR:55;
hence ex c being Element of X st
( LIN a,b,c & a <> c & b <> c ) by A6, A7; :: thesis: verum