let AP be AffinPlane; ( AP is satisfying_DES1_1 implies AP is satisfying_DES1 )
assume A1:
AP is satisfying_DES1_1
; AP is satisfying_DES1
let A be Subset of AP; AFF_3:def 1 for P, C being Subset of AP
for o, a, a9, b, b9, c, c9, p, q being Element of AP 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 & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let P, C be Subset of AP; for o, a, a9, b, b9, c, c9, p, q being Element of AP 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 & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 holds
a,c // p,q
let o, a, a9, b, b9, c, c9, p, q be Element of AP; ( A is being_line & P is being_line & C is being_line & P <> A & P <> C & A <> C & o in A & a in A & a9 in A & o in P & b in P & b9 in P & o in C & c in C & c9 in C & o <> a & o <> b & o <> c & p <> q & not LIN b,a,c & not LIN b9,a9,c9 & a <> a9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // a9,c9 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:
a9 in A
and
A11:
o in P
and
A12:
b in P
and
A13:
b9 in P
and
A14:
o in C
and
A15:
c in C
and
A16:
c9 in C
and
A17:
o <> a
and
A18:
o <> b
and
A19:
o <> c
and
A20:
p <> q
and
A21:
not LIN b,a,c
and
A22:
not LIN b9,a9,c9
and
A23:
a <> a9
and
A24:
LIN b,a,p
and
A25:
LIN b9,a9,p
and
A26:
LIN b,c,q
and
A27:
LIN b9,c9,q
and
A28:
a,c // a9,c9
; a,c // p,q
A29:
a9 <> b9
by A22, AFF_1:16;
set M = Line b,c;
A30:
c in Line b,c
by AFF_1:26;
then A31:
Line b,c <> P
by A3, A4, A6, A11, A14, A15, A19, AFF_1:30;
A32:
Line b,c <> P
by A3, A4, A6, A11, A14, A15, A19, A30, AFF_1:30;
A33:
b in Line b,c
by AFF_1:26;
set K = Line b,a;
A34:
a in Line b,a
by AFF_1:26;
then A35:
Line b,a <> P
by A2, A3, A5, A8, A9, A11, A17, AFF_1:30;
A36:
p in Line b,a
by A24, AFF_1:def 2;
A37:
( a9 <> c9 & b <> a )
by A21, A22, AFF_1:16;
A38:
b <> c
by A21, AFF_1:16;
A39:
q in Line b,c
by A26, AFF_1:def 2;
A40:
b9 <> c9
by A22, AFF_1:16;
A41:
b in Line b,a
by AFF_1:26;
A42:
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;
A43:
c <> c9
proof
assume
c = c9
;
contradiction
then A44:
c,
a // c,
a9
by A28, AFF_1:13;
(
LIN o,
a,
a9 & not
LIN o,
c,
a )
by A2, A8, A9, A10, A42, AFF_1:15, AFF_1:33;
hence
contradiction
by A23, A44, AFF_1:23;
verum
end;
b <> c
by A21, AFF_1:16;
then A45:
Line b,c is being_line
by AFF_1:def 3;
b <> a
by A21, AFF_1:16;
then A46:
Line b,a is being_line
by AFF_1:def 3;
A47:
Line b,a <> P
by A2, A3, A5, A8, A9, A11, A17, A34, AFF_1:30;
A48:
now set C9 =
Line b9,
c9;
set A9 =
Line b9,
a9;
A49:
c9 in Line b9,
c9
by AFF_1:26;
A50:
(
Line b9,
a9 is
being_line &
b9 in Line b9,
a9 )
by A29, AFF_1:26, AFF_1:def 3;
A51:
a9 in Line b9,
a9
by AFF_1:26;
then A52:
Line b9,
a9 <> Line b9,
c9
by A22, A50, A49, AFF_1:33;
A53:
q in Line b9,
c9
by A27, AFF_1:def 2;
A54:
p in Line b9,
a9
by A25, AFF_1:def 2;
A55:
(
Line b9,
c9 is
being_line &
b9 in Line b9,
c9 )
by A40, AFF_1:26, AFF_1:def 3;
assume A56:
LIN b9,
p,
q
;
a,c // p,qthen A57:
LIN b9,
q,
p
by AFF_1:15;
A58:
now A59:
Line b9,
c9 <> Line b,
c
proof
assume
Line b9,
c9 = Line b,
c
;
contradiction
then
LIN c,
c9,
b
by A45, A33, A30, A49, AFF_1:33;
then
b in C
by A4, A15, A16, A43, AFF_1:39;
hence
contradiction
by A3, A4, A6, A11, A12, A14, A18, AFF_1:30;
verum
end; assume
b9 <> q
;
a,c // p,qthen A60:
p in Line b9,
c9
by A57, A55, A53, AFF_1:39;
then
LIN b,
a,
b9
by A24, A50, A54, A55, A52, AFF_1:30;
then
b9 in Line b,
a
by AFF_1:def 2;
then A61:
b = b9
by A3, A12, A13, A46, A41, A47, AFF_1:30;
p = b9
by A50, A54, A55, A52, A60, AFF_1:30;
then
p = q
by A45, A33, A39, A55, A53, A61, A59, AFF_1:30;
hence
a,
c // p,
q
by AFF_1:12;
verum end; now A62:
Line b9,
a9 <> Line b,
a
proof
assume
Line b9,
a9 = Line b,
a
;
contradiction
then
LIN a,
a9,
b
by A46, A41, A34, A51, AFF_1:33;
then
b in A
by A2, A9, A10, A23, AFF_1:39;
hence
contradiction
by A2, A3, A5, A8, A11, A12, A18, AFF_1:30;
verum
end; assume
b9 <> p
;
a,c // p,qthen A63:
q in Line b9,
a9
by A56, A50, A54, AFF_1:39;
then
LIN b,
c,
b9
by A26, A50, A55, A53, A52, AFF_1:30;
then
b9 in Line b,
c
by AFF_1:def 2;
then A64:
b = b9
by A3, A12, A13, A45, A33, A32, AFF_1:30;
q = b9
by A50, A55, A53, A52, A63, AFF_1:30;
then
p = q
by A46, A41, A36, A50, A54, A64, A62, AFF_1:30;
hence
a,
c // p,
q
by AFF_1:12;
verum end; hence
a,
c // p,
q
by A20, A58;
verum end;
A65:
Line b,a <> Line b,c
by A21, A46, A41, A34, A30, AFF_1:33;
now A66:
(
LIN o,
c,
c9 &
LIN b9,
q,
c9 )
by A4, A14, A15, A16, A27, AFF_1:15, AFF_1:33;
assume A67:
not
LIN b9,
p,
q
;
a,c // p,q
(
LIN o,
a,
a9 &
LIN b9,
p,
a9 )
by A2, A8, A9, A10, A25, AFF_1:15, AFF_1:33;
hence
a,
c // p,
q
by A1, A3, A11, A12, A13, A18, A28, A46, A45, A41, A34, A33, A30, A36, A39, A31, A35, A37, A38, A65, A42, A43, A67, A66, Def2;
verum end;
hence
a,c // p,q
by A48; verum