let X be OrtAfPl; :: thesis: for a, b being Element of X st a <> b holds
ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )
let a, b be Element of X; :: thesis: ( a <> b implies ex c being Element of X st
( LIN a,b,c & a <> c & b <> c ) )
assume A1: a <> b ; :: 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
A2: ( LIN p,q,r & p <> q & q <> r & 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 A2, ANALMETR:55;
then consider c' being Element of the carrier of (Af X) such that
A3: ( LIN a',b',c' & a' <> c' & b' <> c' ) by A1, A2, TRANSLAC:2;
reconsider c = c' as Element of X by ANALMETR:47;
LIN a,b,c by A3, ANALMETR:55;
hence ex c being Element of X st
( LIN a,b,c & a <> c & b <> c ) by A3; :: thesis: verum