let POS be OrtAfPl; 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; ( 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
; ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
A2:
now ( 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 )
;
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 )
;
verum end;
LIN a9,b9,a9
by AFF_1:7;
then A4:
LIN a,b,a
by Th40;
A5:
now ( c = d implies ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) )assume
c = d
;
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;
verum end;
LIN c9,d9,c9
by AFF_1:7;
then A6:
LIN c,d,c
by Th40;
now ( a = b implies ex p being Element of POS st
( LIN a,b,p & LIN c,d,p ) )assume
a = b
;
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;
verum end;
hence
ex p being Element of POS st
( LIN a,b,p & LIN c,d,p )
by A5, A2; verum