let MS be OrtAfPl; :: thesis: for a, b, c, d being Element of MS
for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )
let a, b, c, d be Element of MS; :: thesis: for K being Subset of the carrier of MS st a,b _|_ K & c,d _|_ K holds
( a,b // c,d & a,b // d,c )
let K be Subset of MS; :: thesis: ( a,b _|_ K & c,d _|_ K implies ( a,b // c,d & a,b // d,c ) )
assume that
A1: a,b _|_ K and
A2: c,d _|_ K ; :: thesis: ( a,b // c,d & a,b // d,c )
reconsider K9 = K as Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
K is being_line by A1, ANALMETR:44;
then K9 is being_line by ANALMETR:43;
then consider p9, q9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A3: ( p9 in K9 & q9 in K9 ) and
A4: p9 <> q9 by AFF_1:19;
reconsider p = p9, q = q9 as Element of MS ;
( a,b _|_ p,q & c,d _|_ p,q ) by A1, A2, A3, ANALMETR:53;
hence a,b // c,d by A4, ANALMETR:63; :: thesis: a,b // d,c
hence a,b // d,c by ANALMETR:59; :: thesis: verum