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 AffinStruct(# the carrier of POS, the CONGR of 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 :: thesis: ( a <> b & c <> d implies ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) )

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, Th45;
then consider p being Element of POS such that
A3: ( p in Line (a,b) & p in Line (c,d) ) by Th66;
( LIN a,b,p & LIN c,d,p ) by A3, Def10;
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:7;
then A4: LIN a,b,a by Th40;

A5: now :: thesis: ( c = d implies ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) )

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 Th58;
then LIN c,d,a ;
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:7;
then A6: LIN c,d,c by Th40;

now :: thesis: ( a = b implies ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) )

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 Th58;
then LIN a,b,c ;
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