let AP be AffinPlane; :: thesis: ( AP is satisfying_DES1_2 implies AP is satisfying_DES1_3 )
assume A1:
AP is satisfying_DES1_2
; :: thesis: AP is satisfying_DES1_3
let A be Subset of AP; :: according to AFF_3:def 4 :: thesis: for P, C being Subset of AP
for o, a, a', b, b', c, c', 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 & a' in A & 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' & b <> b' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in P
let P, C be Subset of AP; :: thesis: for o, a, a', b, b', c, c', 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 & a' in A & 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' & b <> b' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q holds
o in P
let o, a, a', b, b', c, c', p, q be Element of AP; :: thesis: ( 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 & 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' & b <> b' & a <> a' & LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q implies o in P )
assume that
A2:
( A is being_line & P is being_line & C is being_line )
and
A3:
( P <> A & P <> C & A <> C )
and
A4:
( o in A & a in A & a' in A & 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' & b <> b' & a <> a' )
and
A5:
( LIN b,a,p & LIN b',a',p & LIN b,c,q & LIN b',c',q & a,c // a',c' & a,c // p,q )
; :: thesis: o in P
assume A6:
not o in P
; :: thesis: contradiction
A7:
( a <> b & a <> c & b <> c & a' <> b' & a' <> c' & b' <> c' )
by A4, AFF_1:16;
A8:
not LIN o,c,a
A9:
c <> c'
proof
assume
c = c'
;
:: thesis: contradiction
then
(
LIN o,
a,
a' &
c,
a // c,
a' )
by A2, A4, A5, AFF_1:13, AFF_1:33;
hence
contradiction
by A4, A8, AFF_1:23;
:: thesis: verum
end;
A10:
a',c' // p,q
by A5, A7, AFF_1:14;
A11:
( p <> b & p <> b' & q <> b & q <> b' )
proof
assume A12:
( not
p <> b or not
p <> b' or not
q <> b or not
q <> b' )
;
:: thesis: contradiction
A13:
now assume A14:
b = q
;
:: thesis: contradiction
( not
LIN b,
c,
a &
c,
a // q,
p )
by A4, A5, AFF_1:13, AFF_1:15;
hence
contradiction
by A4, A5, A14, AFF_1:69;
:: thesis: verum end;
now assume A15:
b' = q
;
:: thesis: contradiction
( not
LIN b',
c',
a' &
c',
a' // q,
p )
by A4, A10, AFF_1:13, AFF_1:15;
hence
contradiction
by A4, A5, A15, AFF_1:69;
:: thesis: verum end;
hence
contradiction
by A4, A5, A10, A12, A13, AFF_1:69;
:: thesis: verum
end;
A16:
( not P // A or not C // P )
set D = Line b,c;
set T = Line b,a;
set N = Line p,q;
set M = Line a',c';
set K = Line b',a';
A17:
( Line b,c is being_line & Line b,a is being_line & Line p,q is being_line & Line a',c' is being_line & Line b',a' is being_line & p in Line p,q & q in Line p,q & b in Line b,c & c in Line b,c & b in Line b,a & a in Line b,a & a' in Line a',c' & c' in Line a',c' & b' in Line b',a' & a' in Line b',a' )
by A4, A7, AFF_1:38;
then A18:
( q in Line b,c & p in Line b,a & p in Line b',a' )
by A5, A7, AFF_1:39;
A19:
now assume
not
P // A
;
:: thesis: contradictionthen consider x being
Element of
AP such that A20:
(
x in P &
x in A )
by A2, AFF_1:72;
A21:
x <> a
proof
assume A22:
x = a
;
:: thesis: contradiction
then A23:
(
p in P &
a in P )
by A2, A4, A5, A7, A20, AFF_1:39;
Line b',
a' <> P
by A2, A3, A4, A17, A20, A22, AFF_1:30;
hence
contradiction
by A2, A4, A11, A17, A18, A23, AFF_1:30;
:: thesis: verum
end;
x <> b
proof
assume A24:
x = b
;
:: thesis: contradiction
then
p in A
by A2, A4, A5, A7, A20, AFF_1:39;
then
(
a',
c' // a',
q or
b' in A )
by A2, A4, A10, A17, A18, AFF_1:30;
then
LIN a',
c',
q
by A2, A3, A4, A20, A24, AFF_1:30, AFF_1:def 1;
then
(
LIN q,
c',
a' &
LIN q,
c',
b' &
LIN q,
c',
c' )
by A5, AFF_1:15, AFF_1:16;
then
q = c'
by A4, AFF_1:17;
then
LIN c,
c',
b
by A5, AFF_1:15;
then
b in C
by A2, A4, A9, AFF_1:39;
hence
contradiction
by A2, A3, A4, A20, A24, AFF_1:30;
:: thesis: verum
end; then
x in C
by A1, A2, A3, A4, A5, A9, A20, A21, Def3;
hence
contradiction
by A2, A3, A4, A6, A20, AFF_1:30;
:: thesis: verum end;
now assume
not
C // P
;
:: thesis: contradictionthen consider x being
Element of
AP such that A25:
(
x in C &
x in P )
by A2, AFF_1:72;
A26:
x <> c
proof
assume A27:
x = c
;
:: thesis: contradiction
then
(
LIN b,
c,
b' &
LIN b,
c,
c )
by A2, A4, A25, AFF_1:33;
then
(
LIN q,
b',
c &
LIN q,
b',
c' &
LIN q,
b',
b' )
by A5, A7, AFF_1:15, AFF_1:17;
then A28:
b' in C
by A2, A4, A9, A11, AFF_1:17, AFF_1:39;
then A29:
c = b'
by A2, A3, A4, A25, A27, AFF_1:30;
LIN c,
c',
q
by A2, A3, A4, A5, A25, A27, A28, AFF_1:30;
then
q in C
by A2, A4, A9, AFF_1:39;
then
C = Line b,
c
by A2, A4, A11, A17, A18, A29, AFF_1:30;
hence
contradiction
by A2, A3, A4, A17, A28, AFF_1:30;
:: thesis: verum
end; A30:
x <> b
proof
assume A31:
x = b
;
:: thesis: contradiction
then
(
LIN b,
c,
c' &
LIN b,
c,
c )
by A2, A4, A25, AFF_1:33;
then
LIN c,
c',
q
by A5, A7, AFF_1:17;
then
(
q in C &
LIN q,
c',
b' )
by A2, A4, A5, A9, AFF_1:15, AFF_1:39;
then
(
q = c' or
b' in C )
by A2, A4, AFF_1:39;
then
c',
a' // c',
p
by A2, A3, A4, A10, A25, A31, AFF_1:13, AFF_1:30;
then
LIN c',
a',
p
by AFF_1:def 1;
then
(
LIN p,
a',
c' &
LIN p,
a',
b' &
LIN p,
a',
a' )
by A5, AFF_1:15, AFF_1:16;
then
p = a'
by A4, AFF_1:17;
then
LIN a,
a',
b
by A5, AFF_1:15;
then
b in A
by A2, A4, AFF_1:39;
hence
contradiction
by A2, A3, A4, A25, A31, AFF_1:30;
:: thesis: verum
end; A32:
( not
LIN b,
c,
a & not
LIN b',
c',
a' )
by A4, AFF_1:15;
(
c,
a // q,
p &
c,
a // c',
a' )
by A5, AFF_1:13;
then
x in A
by A1, A2, A3, A4, A5, A25, A26, A30, A32, Def3;
hence
contradiction
by A2, A3, A4, A6, A25, AFF_1:30;
:: thesis: verum end;
hence
contradiction
by A16, A19; :: thesis: verum