let POS be OrtAfPl; :: thesis: for a, b, c, d being Element of POS st a,b _|_ c,d holds
ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
let a, b, c, d be Element of POS; :: thesis: ( a,b _|_ c,d implies ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) )
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of (Af POS) ;
assume A1: a,b _|_ c,d ; :: thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )

A2: now

set M = Line (a,b);
set N = Line (c,d);
assume ( a <> b & c <> d ) ; :: thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
then Line (a,b) _|_ Line (c,d) by A1, Th63;
then consider p being Element of POS such that
A3: ( p in Line (a,b) & p in Line (c,d) ) by Th88;
( LIN a,b,p & LIN c,d,p ) by A3, Def12;
hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) ; :: thesis: verum

end;

LIN a9,b9,a9 by AFF_1:16;
then A4: LIN a,b,a by Th55;

A5: now

assume c = d ; :: thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
then c,d // c,a by Th80;
then LIN c,d,a by Def11;
hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) by A4; :: thesis: verum

end;

LIN c9,d9,c9 by AFF_1:16;
then A6: LIN c,d,c by Th55;

now

assume a = b ; :: thesis: ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
then a,b // a,c by Th80;
then LIN a,b,c by Def11;
hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) by A6; :: thesis: verum

end;

hence ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) by A5, A2; :: thesis: verum