let POS be OrtAfPl; :: thesis: for a, b, c, d being Element of st a,b _|_ c,d holds
ex p being Element of st
( LIN a,b,p & LIN c,d,p )
let a, b, c, d be Element of ; :: thesis: ( a,b _|_ c,d implies ex p being Element of st
( LIN a,b,p & LIN c,d,p ) )
reconsider a' = a, b' = b, c' = c, d' = d as Element of ;
assume A1: a,b _|_ c,d ; :: thesis: ex p being Element of 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 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 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 st
( LIN a,b,p & LIN c,d,p ) ; :: thesis: verum

end;

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

A5: now

assume c = d ; :: thesis: ex p being Element of 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 st
( LIN a,b,p & LIN c,d,p ) by A4; :: thesis: verum

end;

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

now

assume a = b ; :: thesis: ex p being Element of 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 st
( LIN a,b,p & LIN c,d,p ) by A6; :: thesis: verum

end;

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