let AS be AffinSpace; :: thesis: for a, b, a9, b9, p being Element of AS

for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

let a, b, a9, b9, p be Element of AS; :: thesis: for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

let M, N, P, Q be Subset of AS; :: thesis: ( p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q implies ex q being Element of AS st

( q in P & q in Q ) )

assume that

A1: p in M and

A2: a in M and

A3: b in M and

A4: p in N and

A5: a9 in N and

A6: b9 in N and

A7: not p in P and

A8: not p in Q and

A9: M <> N and

A10: a in P and

A11: a9 in P and

A12: b in Q and

A13: b9 in Q and

A14: M is being_line and

A15: N is being_line and

A16: P is being_line and

A17: Q is being_line ; :: thesis: ( P // Q or ex q being Element of AS st

( q in P & q in Q ) )

A18: a <> a9 by A1, A2, A4, A5, A7, A9, A10, A14, A15, AFF_1:18;

LIN p,a,b by A1, A2, A3, A14, AFF_1:21;

then consider c being Element of AS such that

A19: LIN p,a9,c and

A20: a,a9 // b,c by A7, A10, Th1;

set D = Line (b,c);

A21: b in Line (b,c) by AFF_1:15;

A22: c in Line (b,c) by AFF_1:15;

A23: b <> b9 by A1, A3, A4, A6, A8, A9, A12, A14, A15, AFF_1:18;

A24: c in N by A4, A5, A7, A11, A15, A19, AFF_1:25;

then A25: b <> c by A1, A3, A4, A8, A9, A12, A14, A15, AFF_1:18;

then A26: Line (b,c) is being_line by AFF_1:def 3;

( q in P & q in Q ) ) by A10, A11, A12, A16, A17, A18, A20, A25, A22, AFF_1:38; :: thesis: verum

for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

let a, b, a9, b9, p be Element of AS; :: thesis: for M, N, P, Q being Subset of AS st p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q holds

ex q being Element of AS st

( q in P & q in Q )

let M, N, P, Q be Subset of AS; :: thesis: ( p in M & a in M & b in M & p in N & a9 in N & b9 in N & not p in P & not p in Q & M <> N & a in P & a9 in P & b in Q & b9 in Q & M is being_line & N is being_line & P is being_line & Q is being_line & not P // Q implies ex q being Element of AS st

( q in P & q in Q ) )

assume that

A1: p in M and

A2: a in M and

A3: b in M and

A4: p in N and

A5: a9 in N and

A6: b9 in N and

A7: not p in P and

A8: not p in Q and

A9: M <> N and

A10: a in P and

A11: a9 in P and

A12: b in Q and

A13: b9 in Q and

A14: M is being_line and

A15: N is being_line and

A16: P is being_line and

A17: Q is being_line ; :: thesis: ( P // Q or ex q being Element of AS st

( q in P & q in Q ) )

A18: a <> a9 by A1, A2, A4, A5, A7, A9, A10, A14, A15, AFF_1:18;

LIN p,a,b by A1, A2, A3, A14, AFF_1:21;

then consider c being Element of AS such that

A19: LIN p,a9,c and

A20: a,a9 // b,c by A7, A10, Th1;

set D = Line (b,c);

A21: b in Line (b,c) by AFF_1:15;

A22: c in Line (b,c) by AFF_1:15;

A23: b <> b9 by A1, A3, A4, A6, A8, A9, A12, A14, A15, AFF_1:18;

A24: c in N by A4, A5, A7, A11, A15, A19, AFF_1:25;

then A25: b <> c by A1, A3, A4, A8, A9, A12, A14, A15, AFF_1:18;

then A26: Line (b,c) is being_line by AFF_1:def 3;

now :: thesis: ( Line (b,c) <> Q implies ex q being Element of AS st

( q in P & q in Q ) )

hence
( P // Q or ex q being Element of AS st ( q in P & q in Q ) )

assume
Line (b,c) <> Q
; :: thesis: ex q being Element of AS st

( q in P & q in Q )

then A27: c <> b9 by A12, A13, A17, A23, A26, A21, A22, AFF_1:18;

LIN b9,c,a9 by A5, A6, A15, A24, AFF_1:21;

then consider q being Element of AS such that

A28: LIN b9,b,q and

A29: c,b // a9,q by A27, Th1;

a9,a // c,b by A20, AFF_1:4;

then a9,a // a9,q by A25, A29, AFF_1:5;

then LIN a9,a,q by AFF_1:def 1;

then A30: q in P by A10, A11, A16, A18, AFF_1:25;

q in Q by A12, A13, A17, A23, A28, AFF_1:25;

hence ex q being Element of AS st

( q in P & q in Q ) by A30; :: thesis: verum

end;( q in P & q in Q )

then A27: c <> b9 by A12, A13, A17, A23, A26, A21, A22, AFF_1:18;

LIN b9,c,a9 by A5, A6, A15, A24, AFF_1:21;

then consider q being Element of AS such that

A28: LIN b9,b,q and

A29: c,b // a9,q by A27, Th1;

a9,a // c,b by A20, AFF_1:4;

then a9,a // a9,q by A25, A29, AFF_1:5;

then LIN a9,a,q by AFF_1:def 1;

then A30: q in P by A10, A11, A16, A18, AFF_1:25;

q in Q by A12, A13, A17, A23, A28, AFF_1:25;

hence ex q being Element of AS st

( q in P & q in Q ) by A30; :: thesis: verum

( q in P & q in Q ) ) by A10, A11, A12, A16, A17, A18, A20, A25, A22, AFF_1:38; :: thesis: verum