let AP be AffinPlane; ( AP is Desarguesian implies AP is satisfying_DES1 )
assume A1:
AP is Desarguesian
; AP is satisfying_DES1
let A be Subset of ; AFF_3:def 1 for P, C being Subset of
for o, a, a', b, b', c, c', p, q being Element of st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q
let P, C be Subset of ; for o, a, a', b, b', c, c', p, q being Element of st A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' holds
a,c // p,q
let o, a, a', b, b', c, c', p, q be Element of ; ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a' in A & o in P & b in P & b' in P & o in C & c in C & c' in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b',a',c' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' implies a,c // p,q )
assume that
A2:
A is being_line
and
A3:
P is being_line
and
A4:
C is being_line
and
A5:
P <> A
and
A6:
P <> C
and
A7:
A <> C
and
A8:
o in A
and
A9:
a in A
and
A10:
a' in A
and
A11:
o in P
and
A12:
b in P
and
A13:
b' in P
and
A14:
o in C
and
A15:
c in C
and
A16:
c' in C
and
A17:
o <> a
and
A18:
o <> b
and
A19:
o <> c
and
p <> q
and
A20:
not LIN b,a,c
and
A21:
not LIN b',a',c'
and
A22:
a <> a'
and
A23:
LIN b,a,p
and
A24:
LIN b',a',p
and
A25:
LIN b,c,q
and
A26:
LIN b',c',q
and
A27:
a,c // a',c'
; a,c // p,q
set D = Line b,c;
b <> c
by A20, AFF_1:16;
then
Line b,c is being_line
by AFF_1:def 3;
then consider D' being Subset of such that
A28:
c' in D'
and
A29:
Line b,c // D'
by AFF_1:63;
A30:
D' is being_line
by A29, AFF_1:50;
set M = Line b',c';
A31:
q in Line b',c'
by A26, AFF_1:def 2;
A32:
b in Line b,c
by AFF_1:26;
A33:
c in Line b,c
by AFF_1:26;
not D' // P
proof
assume
D' // P
;
contradiction
then
Line b,
c // P
by A29, AFF_1:58;
then
c in P
by A12, A32, A33, AFF_1:59;
hence
contradiction
by A3, A4, A6, A11, A14, A15, A19, AFF_1:30;
verum
end;
then consider d being Element of such that
A34:
d in D'
and
A35:
d in P
by A3, A30, AFF_1:72;
A36:
q in Line b,c
by A25, AFF_1:def 2;
then A37:
d,c' // b,q
by A32, A28, A29, A34, AFF_1:53;
A38:
( a <> b & b,a // b,p )
by A20, A23, AFF_1:16, AFF_1:def 1;
A39:
c,a // c',a'
by A27, AFF_1:13;
c,b // c',d
by A32, A33, A28, A29, A34, AFF_1:53;
then
b,a // d,a'
by A1, A2, A3, A4, A6, A7, A8, A9, A10, A11, A12, A14, A15, A16, A17, A18, A19, A35, A39, AFF_2:def 4;
then A40:
d,a' // b,p
by A38, AFF_1:14;
set K = Line b',a';
A41:
( b' in Line b',a' & p in Line b',a' )
by A24, AFF_1:26, AFF_1:def 2;
A42:
a' <> b'
by A21, AFF_1:16;
then A43:
Line b',a' is being_line
by AFF_1:def 3;
A44:
b' in Line b',c'
by AFF_1:26;
A45:
c' in Line b',c'
by AFF_1:26;
A46:
b' <> c'
by A21, AFF_1:16;
then A47:
Line b',c' is being_line
by AFF_1:def 3;
A48:
not LIN o,a,c
proof
assume
LIN o,
a,
c
;
contradiction
then
c in A
by A2, A8, A9, A17, AFF_1:39;
hence
contradiction
by A2, A4, A7, A8, A14, A15, A19, AFF_1:30;
verum
end;
A49:
c <> c'
proof
assume
c = c'
;
contradiction
then A50:
c,
a // c,
a'
by A27, AFF_1:13;
(
LIN o,
a,
a' & not
LIN o,
c,
a )
by A2, A8, A9, A10, A48, AFF_1:15, AFF_1:33;
hence
contradiction
by A22, A50, AFF_1:23;
verum
end;
A51:
d <> b'
proof
assume
d = b'
;
contradiction
then
Line b',
c' = D'
by A46, A47, A44, A45, A28, A30, A34, AFF_1:30;
then
Line b,
c = Line b',
c'
by A31, A36, A29, AFF_1:59;
then
LIN c,
c',
b
by A47, A45, A32, A33, AFF_1:33;
then
b in C
by A4, A15, A16, A49, AFF_1:39;
hence
contradiction
by A3, A4, A6, A11, A12, A14, A18, AFF_1:30;
verum
end;
A52:
a' <> c'
by A21, AFF_1:16;
A53:
o <> a'
proof
assume A54:
o = a'
;
contradiction
LIN o,
c,
c'
by A4, A14, A15, A16, AFF_1:33;
hence
contradiction
by A27, A52, A48, A54, AFF_1:69;
verum
end;
o <> c'
proof
A55:
not
LIN o,
c,
a
by A48, AFF_1:15;
assume A56:
o = c'
;
contradiction
(
LIN o,
a,
a' &
c,
a // c',
a' )
by A2, A8, A9, A10, A27, AFF_1:13, AFF_1:33;
hence
contradiction
by A53, A56, A55, AFF_1:69;
verum
end;
then A57:
Line b',c' <> P
by A3, A4, A6, A11, A14, A16, A45, AFF_1:30;
A58:
a' in Line b',a'
by AFF_1:26;
then
Line b',a' <> P
by A2, A3, A5, A8, A10, A11, A53, AFF_1:30;
then
a',c' // p,q
by A1, A3, A12, A13, A42, A46, A43, A47, A58, A41, A44, A45, A31, A57, A35, A51, A40, A37, AFF_2:def 4;
hence
a,c // p,q
by A27, A52, AFF_1:14; verum