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 A1: ( a,b _|_ K & c,d _|_ K ) ; :: thesis: ( a,b // c,d & a,b // d,c )
reconsider K' = K as Subset of (Af MS) by ANALMETR:57;
K is being_line by A1, ANALMETR:62;
then K' is being_line by ANALMETR:58;
then consider p', q' being Element of (Af MS) such that
A2: ( p' in K' & q' in K' ) and
A3: p' <> q' by AFF_1:31;
reconsider p = p', q = q' as Element of MS by ANALMETR:47;
( a,b _|_ p,q & c,d _|_ p,q ) by A1, A2, ANALMETR:75;
hence a,b // c,d by A3, ANALMETR:85; :: thesis: a,b // d,c
hence a,b // d,c by ANALMETR:81; :: thesis: verum