let X be OrtAfPl; for a, b being Element of ex c being Element of st
( LIN a,b,c & a <> c & b <> c )
let a, b be Element of ; ex c being Element of st
( LIN a,b,c & a <> c & b <> c )
consider p, q, r being Element of 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 by ANALMETR:47;
LIN p',q',r'
by A1, ANALMETR:55;
then consider c' being Element of 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 by ANALMETR:47;
LIN a,b,c
by A5, ANALMETR:55;
hence
ex c being Element of st
( LIN a,b,c & a <> c & b <> c )
by A6, A7; verum