let AP be AffinPlane; ( AP is satisfying_DES1 implies AP is satisfying_DES1_1 )
assume A1:
AP is satisfying_DES1
; AP is satisfying_DES1_1
let A be Subset of AP; AFF_3:def 2 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 & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
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 & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q holds
a,c // a9,c9
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 & c <> q & not LIN b,a,c & not LIN b9,a9,c9 & LIN b,a,p & LIN b9,a9,p & LIN b,c,q & LIN b9,c9,q & a,c // p,q implies a,c // a9,c9 )
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 & b9 in P )
and
A13:
( o in C & c in C )
and
A14:
c9 in C
and
A15:
o <> a
and
A16:
o <> b
and
A17:
o <> c
and
A18:
p <> q
and
A19:
c <> q
and
A20:
not LIN b,a,c
and
A21:
not LIN b9,a9,c9
and
A22:
LIN b,a,p
and
A23:
LIN b9,a9,p
and
A24:
LIN b,c,q
and
A25:
LIN b9,c9,q
and
A26:
a,c // p,q
; a,c // a9,c9
A27:
( LIN o,a,a9 & LIN b9,p,a9 )
by A2, A8, A9, A10, A23, AFF_1:6, AFF_1:21;
set K = Line (b,a);
A28:
a in Line (b,a)
by AFF_1:15;
then A29:
Line (b,a) <> P
by A2, A3, A5, A8, A9, A11, A15, AFF_1:18;
A30:
not LIN o,a,c
proof
assume
LIN o,
a,
c
;
contradiction
then
c in A
by A2, A8, A9, A15, AFF_1:25;
hence
contradiction
by A2, A4, A7, A8, A13, A17, AFF_1:18;
verum
end;
A31:
p in Line (b,a)
by A22, AFF_1:def 2;
A32:
( LIN o,c,c9 & LIN b9,q,c9 )
by A4, A13, A14, A25, AFF_1:6, AFF_1:21;
A33:
( b <> c & a <> p )
by A19, A20, A24, A26, AFF_1:7, AFF_1:14;
A34:
( a9 <> c9 & b <> a )
by A20, A21, AFF_1:7;
b <> a
by A20, AFF_1:7;
then A35:
Line (b,a) is being_line
by AFF_1:def 3;
set M = Line (b,c);
A36:
c in Line (b,c)
by AFF_1:15;
then A37:
Line (b,c) <> P
by A3, A4, A6, A11, A13, A17, AFF_1:18;
b <> c
by A20, AFF_1:7;
then A38:
Line (b,c) is being_line
by AFF_1:def 3;
A39:
( b in Line (b,c) & q in Line (b,c) )
by A24, AFF_1:15, AFF_1:def 2;
q <> b
proof
assume A40:
q = b
;
contradiction
( not
LIN b,
c,
a &
c,
a // q,
p )
by A20, A26, AFF_1:4, AFF_1:6;
hence
contradiction
by A18, A22, A40, AFF_1:55;
verum
end;
then A41:
q <> b9
by A3, A12, A38, A39, A37, AFF_1:18;
A42:
b in Line (b,a)
by AFF_1:15;
p <> b
by A18, A20, A24, A26, AFF_1:55;
then A43:
p <> b9
by A3, A12, A35, A42, A31, A29, AFF_1:18;
A44:
not LIN b9,p,q
proof
set N =
Line (
p,
q);
A45:
Line (
p,
q) is
being_line
by A18, AFF_1:def 3;
assume
LIN b9,
p,
q
;
contradiction
then
LIN p,
q,
b9
by AFF_1:6;
then A46:
b9 in Line (
p,
q)
by AFF_1:def 2;
(
q in Line (
p,
q) &
LIN q,
b9,
c9 )
by A25, AFF_1:6, AFF_1:15;
then A47:
c9 in Line (
p,
q)
by A41, A45, A46, AFF_1:25;
(
p in Line (
p,
q) &
LIN p,
b9,
a9 )
by A23, AFF_1:6, AFF_1:15;
then
a9 in Line (
p,
q)
by A43, A45, A46, AFF_1:25;
hence
contradiction
by A21, A45, A46, A47, AFF_1:21;
verum
end;
Line (b,a) <> Line (b,c)
by A20, A35, A42, A28, A36, AFF_1:21;
hence
a,c // a9,c9
by A1, A3, A11, A12, A16, A26, A35, A38, A42, A28, A36, A31, A39, A37, A29, A34, A30, A44, A33, A27, A32; verum