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

for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & 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 be Element of AS; :: thesis: for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & 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: ( a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & 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: a in M and

A2: b in M and

A3: a9 in N and

A4: b9 in N and

A5: a in P and

A6: a9 in P and

A7: b in Q and

A8: b9 in Q and

A9: M <> N and

A10: M // N and

A11: P is being_line and

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

( q in P & q in Q ) )

A13: a <> a9 by A1, A3, A9, A10, AFF_1:45;

A14: N is being_line by A10, AFF_1:36;

A15: b <> b9 by A2, A4, A9, A10, AFF_1:45;

A16: M is being_line by A10, AFF_1:36;

( q in P & q in Q ) ) by A5, A7; :: thesis: verum

for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & 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 be Element of AS; :: thesis: for M, N, P, Q being Subset of AS st a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & 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: ( a in M & b in M & a9 in N & b9 in N & a in P & a9 in P & b in Q & b9 in Q & M <> N & M // N & 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: a in M and

A2: b in M and

A3: a9 in N and

A4: b9 in N and

A5: a in P and

A6: a9 in P and

A7: b in Q and

A8: b9 in Q and

A9: M <> N and

A10: M // N and

A11: P is being_line and

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

( q in P & q in Q ) )

A13: a <> a9 by A1, A3, A9, A10, AFF_1:45;

A14: N is being_line by A10, AFF_1:36;

A15: b <> b9 by A2, A4, A9, A10, AFF_1:45;

A16: M is being_line by A10, AFF_1:36;

now :: thesis: ( a <> b & not P // 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 A17:
a <> b
; :: thesis: ( P // Q or ex q being Element of AS st

( q in P & q in Q ) )

consider c being Element of AS such that

A18: a,b // a9,c and

A19: a,a9 // b,c by DIRAF:40;

set D = Line (b,c);

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

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

a,b // N by A1, A2, A10, A16, AFF_1:43, AFF_1:52;

then a9,c // N by A17, A18, AFF_1:32;

then A22: c in N by A3, A14, AFF_1:23;

then A23: b <> c by A2, A9, A10, AFF_1:45;

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

( q in P & q in Q ) ) by A5, A6, A7, A11, A12, A13, A19, A23, A21, AFF_1:38; :: thesis: verum

end;( q in P & q in Q ) )

consider c being Element of AS such that

A18: a,b // a9,c and

A19: a,a9 // b,c by DIRAF:40;

set D = Line (b,c);

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

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

a,b // N by A1, A2, A10, A16, AFF_1:43, AFF_1:52;

then a9,c // N by A17, A18, AFF_1:32;

then A22: c in N by A3, A14, AFF_1:23;

then A23: b <> c by A2, A9, A10, AFF_1:45;

then A24: 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 A25: c <> b9 by A7, A8, A12, A15, A24, A20, A21, AFF_1:18;

LIN b9,c,a9 by A3, A4, A14, A22, AFF_1:21;

then consider q being Element of AS such that

A26: LIN b9,b,q and

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

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

then a9,a // a9,q by A23, A27, AFF_1:5;

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

then A28: q in P by A5, A6, A11, A13, AFF_1:25;

q in Q by A7, A8, A12, A15, A26, AFF_1:25;

hence ex q being Element of AS st

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

end;( q in P & q in Q )

then A25: c <> b9 by A7, A8, A12, A15, A24, A20, A21, AFF_1:18;

LIN b9,c,a9 by A3, A4, A14, A22, AFF_1:21;

then consider q being Element of AS such that

A26: LIN b9,b,q and

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

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

then a9,a // a9,q by A23, A27, AFF_1:5;

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

then A28: q in P by A5, A6, A11, A13, AFF_1:25;

q in Q by A7, A8, A12, A15, A26, AFF_1:25;

hence ex q being Element of AS st

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

( q in P & q in Q ) ) by A5, A6, A7, A11, A12, A13, A19, A23, A21, AFF_1:38; :: thesis: verum

( q in P & q in Q ) ) by A5, A7; :: thesis: verum