let POS be OrtAfSp; :: thesis: for M, N being Subset of
for a, b, c, d being Element of 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 ; :: thesis: for a, b, c, d being Element of 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 ; :: 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 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, Th63;
reconsider a' = a, b' = b, c' = c, d' = d, p1' = p1, q1' = q1, p2' = p2, q2' = q2 as Element of ;
LIN p1,q1,b by A2, A8, Def12;
then A11: LIN p1',q1',b' by Th55;
LIN p1,q1,a by A1, A8, Def12;
then LIN p1',q1',a' by Th55;
then p1',q1' // a',b' by A11, AFF_1:19;
then p1,q1 // a,b by Th48;
then A12: p2,q2 _|_ a,b by A6, A10, Def9;
LIN p2,q2,d by A4, A9, Def12;
then A13: LIN p2',q2',d' by Th55;
LIN p2,q2,c by A3, A9, Def12;
then LIN p2',q2',c' by Th55;
then p2',q2' // c',d' by A13, AFF_1:19;
then p2,q2 // c,d by Th48;
hence a,b _|_ c,d by A7, A12, Def9; :: thesis: verum