let POS be OrtAfSp; :: thesis: for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d
let M, N be Subset of POS; :: thesis: for a, b, c, d being Element of POS st a in M & b in M & c in N & d in N & M _|_ N holds
a,b _|_ c,d
let a, b, c, d be Element of POS; :: thesis: ( a in M & b in M & c in N & d in N & M _|_ N implies a,b _|_ c,d )
assume that
A1: a in M and
A2: b in M and
A3: c in N and
A4: d in N and
A5: M _|_ N ; :: thesis: a,b _|_ c,d
consider p1, q1, p2, q2 being Element of POS such that
A6: p1 <> q1 and
A7: p2 <> q2 and
A8: M = Line (p1,q1) and
A9: N = Line (p2,q2) and
A10: p1,q1 _|_ p2,q2 by A5, Th45;
reconsider a9 = a, b9 = b, c9 = c, d9 = d, p19 = p1, q19 = q1, p29 = p2, q29 = q2 as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
LIN p1,q1,b by A2, A8, Def10;
then A11: LIN p19,q19,b9 by Th40;
LIN p1,q1,a by A1, A8, Def10;
then LIN p19,q19,a9 by Th40;
then p19,q19 // a9,b9 by A11, AFF_1:10;
then p1,q1 // a,b by Th36;
then A12: p2,q2 _|_ a,b by A6, A10, Def7;
LIN p2,q2,d by A4, A9, Def10;
then A13: LIN p29,q29,d9 by Th40;
LIN p2,q2,c by A3, A9, Def10;
then LIN p29,q29,c9 by Th40;
then p29,q29 // c9,d9 by A13, AFF_1:10;
then p2,q2 // c,d by Th36;
hence a,b _|_ c,d by A7, A12, Def7; :: thesis: verum