let POS be OrtAfSp; for K being Subset of POS
for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
let K be Subset of POS; for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
let a, b, c, d be Element of POS; ( a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b implies c,d _|_ K )
assume that
A1:
a,b _|_ K
and
A2:
( a,b // c,d or c,d // a,b )
and
A3:
a <> b
; c,d _|_ K
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
consider p, q being Element of POS such that
A4:
( p <> q & K = Line (p,q) )
and
A5:
a,b _|_ p,q
by A1;
( a9,b9 // c9,d9 or c9,d9 // a9,b9 )
by A2, Th36;
then
a9,b9 // c9,d9
by AFF_1:4;
then
a,b // c,d
by Th36;
then
p,q _|_ c,d
by A3, A5, Def7;
then
c,d _|_ p,q
by Def7;
hence
c,d _|_ K
by A4; verum