:: CONMETR semantic presentation
begin
definition
let X be OrtAfPl;
attrX is satisfying_OPAP means :Def1: :: CONMETR:def 1
for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3;
attrX is satisfying_PAP means :: CONMETR:def 2
for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3;
attrX is satisfying_MH1 means :Def3: :: CONMETR:def 3
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4;
attrX is satisfying_MH2 means :Def4: :: CONMETR:def 4
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4;
attrX is satisfying_TDES means :Def5: :: CONMETR:def 5
for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds
a,c // a1,c1;
attrX is satisfying_SCH means :: CONMETR:def 6
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4;
attrX is satisfying_OSCH means :Def7: :: CONMETR:def 7
for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4;
attrX is satisfying_des means :Def8: :: CONMETR:def 8
for a, a1, b, b1, c, c1 being Element of X st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1;
end;
:: deftheorem Def1 defines satisfying_OPAP CONMETR:def_1_:_
for X being OrtAfPl holds
( X is satisfying_OPAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3 );
:: deftheorem defines satisfying_PAP CONMETR:def_2_:_
for X being OrtAfPl holds
( X is satisfying_PAP iff for o, a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3 );
:: deftheorem Def3 defines satisfying_MH1 CONMETR:def_3_:_
for X being OrtAfPl holds
( X is satisfying_MH1 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4 );
:: deftheorem Def4 defines satisfying_MH2 CONMETR:def_4_:_
for X being OrtAfPl holds
( X is satisfying_MH2 iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b2 in M & b4 in M & a2 in N & a4 in N & b1 in N & b3 in N & not a2 in M & not a4 in M & a1,a2 _|_ b1,b2 & a2,a3 _|_ b2,b3 & a3,a4 _|_ b3,b4 holds
a1,a4 _|_ b1,b4 );
:: deftheorem Def5 defines satisfying_TDES CONMETR:def_5_:_
for X being OrtAfPl holds
( X is satisfying_TDES iff for o, a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds
a,c // a1,c1 );
:: deftheorem defines satisfying_SCH CONMETR:def_6_:_
for X being OrtAfPl holds
( X is satisfying_SCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4 );
:: deftheorem Def7 defines satisfying_OSCH CONMETR:def_7_:_
for X being OrtAfPl holds
( X is satisfying_OSCH iff for a1, a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4 );
:: deftheorem Def8 defines satisfying_des CONMETR:def_8_:_
for X being OrtAfPl holds
( X is satisfying_des iff for a, a1, b, b1, c, c1 being Element of X st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1 );
theorem Th1: :: CONMETR:1
for X being OrtAfPl ex a, b, c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
proof
let X be OrtAfPl; ::_thesis: ex a, b, c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
consider a, p being Element of X such that
A1: a <> p by ANALMETR:39;
consider b being Element of X such that
A2: a,p _|_ p,b and
A3: p <> b by ANALMETR:39;
reconsider a9 = a, b9 = b, p9 = p as Element of (Af X) by ANALMETR:35;
consider c being Element of X such that
A4: p,c _|_ a,b and
A5: LIN a,b,c by ANALMETR:69;
take a ; ::_thesis: ex b, c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
take b ; ::_thesis: ex c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )
take c ; ::_thesis: ( LIN a,b,c & a <> b & b <> c & c <> a )
thus LIN a,b,c by A5; ::_thesis: ( a <> b & b <> c & c <> a )
thus a <> b ::_thesis: ( b <> c & c <> a )
proof
assume not a <> b ; ::_thesis: contradiction
then a,p _|_ a,p by A2, ANALMETR:61;
hence contradiction by A1, ANALMETR:39; ::_thesis: verum
end;
thus b <> c ::_thesis: c <> a
proof
assume not b <> c ; ::_thesis: contradiction
then a,p // a,b by A2, A3, A4, ANALMETR:63;
then LIN a,p,b by ANALMETR:def_10;
then LIN a9,p9,b9 by ANALMETR:40;
then LIN p9,a9,b9 by AFF_1:6;
then LIN p,a,b by ANALMETR:40;
then p,a // p,b by ANALMETR:def_10;
then a,p _|_ p,a by A2, A3, ANALMETR:62;
then a,p _|_ a,p by ANALMETR:61;
hence contradiction by A1, ANALMETR:39; ::_thesis: verum
end;
assume not c <> a ; ::_thesis: contradiction
then a,p _|_ a,b by A4, ANALMETR:61;
then p,b // a,b by A1, A2, ANALMETR:63;
then b,p // b,a by ANALMETR:59;
then LIN b,p,a by ANALMETR:def_10;
then LIN b9,p9,a9 by ANALMETR:40;
then LIN p9,a9,b9 by AFF_1:6;
then LIN p,a,b by ANALMETR:40;
then p,a // p,b by ANALMETR:def_10;
then a,p _|_ p,a by A2, A3, ANALMETR:62;
then a,p _|_ a,p by ANALMETR:61;
hence contradiction by A1, ANALMETR:39; ::_thesis: verum
end;
theorem Th2: :: CONMETR:2
for X being OrtAfPl
for a, b being Element of X ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )
proof
let X be OrtAfPl; ::_thesis: for a, b being Element of X ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )
let a, b be Element of X; ::_thesis: ex c being Element of X st
( LIN a,b,c & a <> c & b <> c )
consider p, q, r being Element of X such that
A1: LIN p,q,r and
A2: p <> q and
A3: q <> r and
A4: r <> p by Th1;
reconsider a9 = a, b9 = b, p9 = p, q9 = q, r9 = r as Element of (Af X) by ANALMETR:35;
LIN p9,q9,r9 by A1, ANALMETR:40;
then consider c9 being Element of (Af X) such that
A5: LIN a9,b9,c9 and
A6: a9 <> c9 and
A7: b9 <> c9 by A2, A3, A4, TRANSLAC:1;
reconsider c = c9 as Element of X by ANALMETR:35;
LIN a,b,c by A5, ANALMETR:40;
hence ex c being Element of X st
( LIN a,b,c & a <> c & b <> c ) by A6, A7; ::_thesis: verum
end;
theorem Th3: :: CONMETR:3
for X being OrtAfPl
for A being Subset of X
for a being Element of X st A is being_line holds
ex K being Subset of X st
( a in K & A _|_ K )
proof
let X be OrtAfPl; ::_thesis: for A being Subset of X
for a being Element of X st A is being_line holds
ex K being Subset of X st
( a in K & A _|_ K )
let A be Subset of X; ::_thesis: for a being Element of X st A is being_line holds
ex K being Subset of X st
( a in K & A _|_ K )
let a be Element of X; ::_thesis: ( A is being_line implies ex K being Subset of X st
( a in K & A _|_ K ) )
assume A is being_line ; ::_thesis: ex K being Subset of X st
( a in K & A _|_ K )
then consider b, c being Element of X such that
A1: b <> c and
A2: A = Line (b,c) by ANALMETR:def_12;
consider d being Element of X such that
A3: b,c _|_ a,d and
A4: a <> d by ANALMETR:39;
reconsider a9 = a, d9 = d as Element of (Af X) by ANALMETR:35;
take K = Line (a,d); ::_thesis: ( a in K & A _|_ K )
K = Line (a9,d9) by ANALMETR:41;
hence a in K by AFF_1:15; ::_thesis: A _|_ K
thus A _|_ K by A1, A2, A3, A4, ANALMETR:45; ::_thesis: verum
end;
theorem Th4: :: CONMETR:4
for X being OrtAfPl
for a, b, c being Element of X
for A being Subset of X st A is being_line & a in A & b in A & c in A holds
LIN a,b,c
proof
let X be OrtAfPl; ::_thesis: for a, b, c being Element of X
for A being Subset of X st A is being_line & a in A & b in A & c in A holds
LIN a,b,c
let a, b, c be Element of X; ::_thesis: for A being Subset of X st A is being_line & a in A & b in A & c in A holds
LIN a,b,c
let A be Subset of X; ::_thesis: ( A is being_line & a in A & b in A & c in A implies LIN a,b,c )
assume that
A1: A is being_line and
A2: a in A and
A3: b in A and
A4: c in A ; ::_thesis: LIN a,b,c
reconsider a9 = a, b9 = b, c9 = c as Element of (Af X) by ANALMETR:35;
reconsider A9 = A as Subset of (Af X) by ANALMETR:42;
A9 is being_line by A1, ANALMETR:43;
then LIN a9,b9,c9 by A2, A3, A4, AFF_1:21;
hence LIN a,b,c by ANALMETR:40; ::_thesis: verum
end;
theorem Th5: :: CONMETR:5
for X being OrtAfPl
for a, b being Element of X
for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds
A = M
proof
let X be OrtAfPl; ::_thesis: for a, b being Element of X
for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds
A = M
let a, b be Element of X; ::_thesis: for A, M being Subset of X st A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b holds
A = M
let A, M be Subset of X; ::_thesis: ( A is being_line & M is being_line & a in A & b in A & a in M & b in M & not a = b implies A = M )
assume that
A1: A is being_line and
A2: M is being_line and
A3: a in A and
A4: b in A and
A5: a in M and
A6: b in M ; ::_thesis: ( a = b or A = M )
reconsider A9 = A, M9 = M as Subset of (Af X) by ANALMETR:42;
A7: M9 is being_line by A2, ANALMETR:43;
assume A8: a <> b ; ::_thesis: A = M
A9 is being_line by A1, ANALMETR:43;
hence A = M by A3, A4, A5, A6, A8, A7, AFF_1:18; ::_thesis: verum
end;
theorem Th6: :: CONMETR:6
for X being OrtAfPl
for a, b, c, d being Element of X
for M being Subset of X
for M9 being Subset of (Af X)
for c9, d9 being Element of (Af X) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b
proof
let X be OrtAfPl; ::_thesis: for a, b, c, d being Element of X
for M being Subset of X
for M9 being Subset of (Af X)
for c9, d9 being Element of (Af X) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b
let a, b, c, d be Element of X; ::_thesis: for M being Subset of X
for M9 being Subset of (Af X)
for c9, d9 being Element of (Af X) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b
let M be Subset of X; ::_thesis: for M9 being Subset of (Af X)
for c9, d9 being Element of (Af X) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b
let M9 be Subset of (Af X); ::_thesis: for c9, d9 being Element of (Af X) st c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 holds
c,d // a,b
let c9, d9 be Element of (Af X); ::_thesis: ( c = c9 & d = d9 & M = M9 & a in M & b in M & c9,d9 // M9 implies c,d // a,b )
assume that
A1: c = c9 and
A2: d = d9 and
A3: M = M9 and
A4: a in M and
A5: b in M and
A6: c9,d9 // M9 ; ::_thesis: c,d // a,b
reconsider a9 = a, b9 = b as Element of (Af X) by ANALMETR:35;
A7: M9 is being_line by A6, AFF_1:26;
then a9,b9 // M9 by A3, A4, A5, AFF_1:52;
then c9,d9 // a9,b9 by A7, A6, AFF_1:31;
hence c,d // a,b by A1, A2, ANALMETR:36; ::_thesis: verum
end;
theorem Th7: :: CONMETR:7
for X being OrtAfPl st X is satisfying_TDES holds
Af X is Moufangian
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_TDES implies Af X is Moufangian )
assume A1: X is satisfying_TDES ; ::_thesis: Af X is Moufangian
let K9 be Subset of (Af X); :: according to AFF_2:def_7 ::_thesis: for b1, b2, b3, b4, b5, b6, b7 being Element of the carrier of (Af X) holds
( not K9 is being_line or not b1 in K9 or not b4 in K9 or not b7 in K9 or b2 in K9 or b1 = b4 or b2 = b3 or not LIN b1,b2,b5 or not LIN b1,b3,b6 or not b2,b3 // b5,b6 or not b2,b4 // b5,b7 or not b2,b3 // K9 or b3,b4 // b6,b7 )
let o9, a9, b9, c9, a19, b19, c19 be Element of (Af X); ::_thesis: ( not K9 is being_line or not o9 in K9 or not c9 in K9 or not c19 in K9 or a9 in K9 or o9 = c9 or a9 = b9 or not LIN o9,a9,a19 or not LIN o9,b9,b19 or not a9,b9 // a19,b19 or not a9,c9 // a19,c19 or not a9,b9 // K9 or b9,c9 // b19,c19 )
assume that
A2: K9 is being_line and
A3: o9 in K9 and
A4: c9 in K9 and
A5: c19 in K9 and
A6: not a9 in K9 and
A7: o9 <> c9 and
A8: a9 <> b9 and
A9: LIN o9,a9,a19 and
A10: LIN o9,b9,b19 and
A11: a9,b9 // a19,b19 and
A12: a9,c9 // a19,c19 and
A13: a9,b9 // K9 ; ::_thesis: b9,c9 // b19,c19
reconsider K = K9 as Subset of X by ANALMETR:42;
reconsider o = o9, a = a9, a1 = a19, b = b9, b1 = b19, c = c9, c1 = c19 as Element of X by ANALMETR:35;
A14: a,c // a1,c1 by A12, ANALMETR:36;
A15: a,b // a1,b1 by A11, ANALMETR:36;
now__::_thesis:_(_not_b_in_K_implies_b9,c9_//_b19,c19_)
A16: now__::_thesis:_(_o_<>_a1_implies_b9,c9_//_b19,c19_)
assume A17: o <> a1 ; ::_thesis: b9,c9 // b19,c19
A18: ( o <> a & o <> b & o <> c & o <> c1 & o <> b1 )
proof
A19: now__::_thesis:_not_o_=_b1
o9,c9 // K9 by A2, A3, A4, AFF_1:23;
then A20: a9,b9 // o9,c9 by A2, A13, AFF_1:31;
assume o = b1 ; ::_thesis: contradiction
then a19,o9 // o9,c9 by A8, A11, A20, DIRAF:40;
then o9,c9 // o9,a19 by AFF_1:4;
then LIN o9,c9,a19 by AFF_1:def_1;
then A21: a19 in K9 by A2, A3, A4, A7, AFF_1:25;
LIN o9,a19,a9 by A9, AFF_1:6;
hence contradiction by A2, A3, A6, A17, A21, AFF_1:25; ::_thesis: verum
end;
A22: now__::_thesis:_not_o_=_c1
o9,a9 // o9,a19 by A9, AFF_1:def_1;
then A23: o9,a19 // a9,o9 by AFF_1:4;
assume o = c1 ; ::_thesis: contradiction
then o9,a19 // a9,c9 by A12, AFF_1:4;
then a9,c9 // a9,o9 by A17, A23, DIRAF:40;
then LIN a9,c9,o9 by AFF_1:def_1;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; ::_thesis: verum
end;
assume ( o = a or o = b or o = c or o = c1 or o = b1 ) ; ::_thesis: contradiction
hence contradiction by A3, A6, A7, A13, A22, A19, AFF_1:35; ::_thesis: verum
end;
A24: now__::_thesis:_(_a_<>_a19_implies_b9,c9_//_b19,c19_)
assume A25: a <> a19 ; ::_thesis: b9,c9 // b19,c19
A26: ( not LIN a,a1,b & not LIN a,a1,c )
proof
A27: now__::_thesis:_not_LIN_a,a1,b
LIN a9,a19,o9 by A9, AFF_1:6;
then a9,a19 // a9,o9 by AFF_1:def_1;
then A28: a,a1 // a,o by ANALMETR:36;
assume LIN a,a1,b ; ::_thesis: contradiction
then a,a1 // a,b by ANALMETR:def_10;
then a,b // a,o by A25, A28, ANALMETR:60;
then A29: a,b // o,a by ANALMETR:59;
a9,b9 // o9,c9 by A2, A3, A4, A7, A13, AFF_1:27;
then a,b // o,c by ANALMETR:36;
then o,c // o,a by A8, A29, ANALMETR:60;
then LIN o,c,a by ANALMETR:def_10;
then LIN o9,c9,a9 by ANALMETR:40;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; ::_thesis: verum
end;
A30: now__::_thesis:_not_LIN_a,a1,c
LIN a9,a19,o9 by A9, AFF_1:6;
then a9,a19 // a9,o9 by AFF_1:def_1;
then A31: a,a1 // a,o by ANALMETR:36;
assume LIN a,a1,c ; ::_thesis: contradiction
then a,a1 // a,c by ANALMETR:def_10;
then a,c // a,o by A25, A31, ANALMETR:60;
then LIN a,c,o by ANALMETR:def_10;
then LIN a9,c9,o9 by ANALMETR:40;
then LIN c9,o9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; ::_thesis: verum
end;
assume ( LIN a,a1,b or LIN a,a1,c ) ; ::_thesis: contradiction
hence contradiction by A27, A30; ::_thesis: verum
end;
A32: LIN o,b,b1 by A10, ANALMETR:40;
o9,c9 // o9,c19 by A2, A3, A4, A5, AFF_1:39, AFF_1:41;
then o,c // o,c1 by ANALMETR:36;
then A33: LIN o,c,c1 by ANALMETR:def_10;
o9,c9 // K9 by A2, A3, A4, AFF_1:40, AFF_1:41;
then a9,b9 // o9,c9 by A2, A13, AFF_1:31;
then b9,a9 // o9,c9 by AFF_1:4;
then A34: b,a // o,c by ANALMETR:36;
A35: b,a // b1,a1 by A15, ANALMETR:59;
LIN o,a,a1 by A9, ANALMETR:40;
then b,c // b1,c1 by A1, A14, A17, A18, A26, A32, A33, A35, A34, Def5;
hence b9,c9 // b19,c19 by ANALMETR:36; ::_thesis: verum
end;
now__::_thesis:_(_a_=_a1_implies_b9,c9_//_b19,c19_)
A36: not LIN o9,a9,c9
proof
assume LIN o9,a9,c9 ; ::_thesis: contradiction
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; ::_thesis: verum
end;
assume A37: a = a1 ; ::_thesis: b9,c9 // b19,c19
o9,c9 // o9,c19 by A2, A3, A4, A5, AFF_1:39, AFF_1:41;
then LIN o9,c9,c19 by AFF_1:def_1;
then A38: c9 = c19 by A12, A37, A36, AFF_1:14;
not LIN o9,a9,b9
proof
assume LIN o9,a9,b9 ; ::_thesis: contradiction
then LIN a9,b9,o9 by AFF_1:6;
then A39: a9,b9 // a9,o9 by AFF_1:def_1;
o9,c9 // K9 by A2, A3, A4, AFF_1:23;
then a9,b9 // o9,c9 by A2, A13, AFF_1:31;
then a9,o9 // o9,c9 by A8, A39, DIRAF:40;
then o9,c9 // o9,a9 by AFF_1:4;
then LIN o9,c9,a9 by AFF_1:def_1;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; ::_thesis: verum
end;
then b9 = b19 by A10, A11, A37, AFF_1:14;
hence b9,c9 // b19,c19 by A38, AFF_1:2; ::_thesis: verum
end;
hence b9,c9 // b19,c19 by A24; ::_thesis: verum
end;
assume A40: not b in K ; ::_thesis: b9,c9 // b19,c19
A41: ( o = a1 implies ( o = b1 & o = c1 ) )
proof
assume that
A42: o = a1 and
A43: ( o <> b1 or o <> c1 ) ; ::_thesis: contradiction
A44: now__::_thesis:_not_o_<>_c1
A45: o9,c19 // a9,c9 by A12, A42, AFF_1:4;
assume A46: o <> c1 ; ::_thesis: contradiction
o9,c19 // o9,c9 by A2, A3, A4, A5, AFF_1:39, AFF_1:41;
then a9,c9 // o9,c9 by A46, A45, DIRAF:40;
then c9,a9 // c9,o9 by AFF_1:4;
then LIN c9,a9,o9 by AFF_1:def_1;
then LIN o9,c9,a9 by AFF_1:6;
hence contradiction by A2, A3, A4, A6, A7, AFF_1:25; ::_thesis: verum
end;
now__::_thesis:_not_o_<>_b1
o9,c9 // K9 by A2, A3, A4, AFF_1:23;
then a9,b9 // o9,c9 by A2, A13, AFF_1:31;
then o9,c9 // o9,b19 by A8, A11, A42, DIRAF:40;
then LIN o9,c9,b19 by AFF_1:def_1;
then A47: b19 in K9 by A2, A3, A4, A7, AFF_1:25;
assume A48: o <> b1 ; ::_thesis: contradiction
LIN o9,b19,b9 by A10, AFF_1:6;
hence contradiction by A2, A3, A40, A48, A47, AFF_1:25; ::_thesis: verum
end;
hence contradiction by A43, A44; ::_thesis: verum
end;
now__::_thesis:_(_o_=_a1_implies_b9,c9_//_b19,c19_)
assume o = a1 ; ::_thesis: b9,c9 // b19,c19
then b,c // b1,c1 by A41, ANALMETR:39;
hence b9,c9 // b19,c19 by ANALMETR:36; ::_thesis: verum
end;
hence b9,c9 // b19,c19 by A16; ::_thesis: verum
end;
hence b9,c9 // b19,c19 by A6, A13, AFF_1:35; ::_thesis: verum
end;
theorem Th8: :: CONMETR:8
for X being OrtAfPl st Af X is translational holds
X is satisfying_des
proof
let X be OrtAfPl; ::_thesis: ( Af X is translational implies X is satisfying_des )
assume A1: Af X is translational ; ::_thesis: X is satisfying_des
let a be Element of X; :: according to CONMETR:def_8 ::_thesis: for a1, b, b1, c, c1 being Element of X st not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 holds
b,c // b1,c1
let a1, b, b1, c, c1 be Element of X; ::_thesis: ( not LIN a,a1,b & not LIN a,a1,c & a,a1 // b,b1 & a,a1 // c,c1 & a,b // a1,b1 & a,c // a1,c1 implies b,c // b1,c1 )
assume that
A2: not LIN a,a1,b and
A3: not LIN a,a1,c and
A4: a,a1 // b,b1 and
A5: a,a1 // c,c1 and
A6: a,b // a1,b1 and
A7: a,c // a1,c1 ; ::_thesis: b,c // b1,c1
reconsider a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1 as Element of (Af X) by ANALMETR:35;
LIN a9,a19,a19 by AFF_1:7;
then consider A9 being Subset of (Af X) such that
A8: A9 is being_line and
A9: a9 in A9 and
A10: a19 in A9 and
a19 in A9 by AFF_1:21;
A11: a9,b9 // a19,b19 by A6, ANALMETR:36;
b,b1 // a,a1 by A4, ANALMETR:59;
then A12: b9,b19 // a9,a19 by ANALMETR:36;
A13: a9 <> a19
proof
assume a9 = a19 ; ::_thesis: contradiction
then LIN a9,a19,b9 by AFF_1:7;
hence contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
then for x9 being Element of (Af X) holds
( x9 in A9 iff LIN a9,a19,x9 ) by A8, A9, A10, AFF_1:21, AFF_1:25;
then A9 = Line (a9,a19) by AFF_1:def_2;
then A14: b9,b19 // A9 by A13, A12, AFF_1:def_4;
A15: a9,c9 // a19,c19 by A7, ANALMETR:36;
c,c1 // a,a1 by A5, ANALMETR:59;
then A16: c9,c19 // a9,a19 by ANALMETR:36;
A17: a9 <> a19
proof
assume a9 = a19 ; ::_thesis: contradiction
then LIN a9,a19,b9 by AFF_1:7;
hence contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
then for x9 being Element of (Af X) holds
( x9 in A9 iff LIN a9,a19,x9 ) by A8, A9, A10, AFF_1:21, AFF_1:25;
then A9 = Line (a9,a19) by AFF_1:def_2;
then A18: c9,c19 // A9 by A17, A16, AFF_1:def_4;
LIN c9,c19,c19 by AFF_1:7;
then consider N9 being Subset of (Af X) such that
A19: N9 is being_line and
A20: c9 in N9 and
A21: c19 in N9 and
c19 in N9 by AFF_1:21;
LIN b9,b19,b19 by AFF_1:7;
then consider M9 being Subset of (Af X) such that
A22: M9 is being_line and
A23: b9 in M9 and
A24: b19 in M9 and
b19 in M9 by AFF_1:21;
A25: ( A9 <> M9 & A9 <> N9 )
proof
assume ( A9 = M9 or A9 = N9 ) ; ::_thesis: contradiction
then ( LIN a9,a19,b9 or LIN a9,a19,c9 ) by A8, A9, A10, A23, A20, AFF_1:21;
hence contradiction by A2, A3, ANALMETR:40; ::_thesis: verum
end;
A26: c9 <> c19
proof
assume c9 = c19 ; ::_thesis: contradiction
then c,a // c,a1 by A7, ANALMETR:59;
then LIN c,a,a1 by ANALMETR:def_10;
then LIN c9,a9,a19 by ANALMETR:40;
then LIN a9,a19,c9 by AFF_1:6;
hence contradiction by A3, ANALMETR:40; ::_thesis: verum
end;
then for x9 being Element of (Af X) holds
( x9 in N9 iff LIN c9,c19,x9 ) by A19, A20, A21, AFF_1:21, AFF_1:25;
then N9 = Line (c9,c19) by AFF_1:def_2;
then A27: A9 // N9 by A18, A26, AFF_1:def_5;
A28: b9 <> b19
proof
assume b9 = b19 ; ::_thesis: contradiction
then b,a // b,a1 by A6, ANALMETR:59;
then LIN b,a,a1 by ANALMETR:def_10;
then LIN b9,a9,a19 by ANALMETR:40;
then LIN a9,a19,b9 by AFF_1:6;
hence contradiction by A2, ANALMETR:40; ::_thesis: verum
end;
then for x9 being Element of (Af X) holds
( x9 in M9 iff LIN b9,b19,x9 ) by A22, A23, A24, AFF_1:21, AFF_1:25;
then M9 = Line (b9,b19) by AFF_1:def_2;
then A9 // M9 by A14, A28, AFF_1:def_5;
then b9,c9 // b19,c19 by A1, A8, A9, A10, A22, A23, A24, A19, A20, A21, A27, A25, A11, A15, AFF_2:def_11;
hence b,c // b1,c1 by ANALMETR:36; ::_thesis: verum
end;
theorem :: CONMETR:9
for X being OrtAfPl st X is satisfying_MH1 holds
X is satisfying_OSCH
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_MH1 implies X is satisfying_OSCH )
assume A1: X is satisfying_MH1 ; ::_thesis: X is satisfying_OSCH
let a1 be Element of X; :: according to CONMETR:def_7 ::_thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let M, N be Subset of X; ::_thesis: ( M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )
assume that
A2: M _|_ N and
A3: a1 in M and
A4: a3 in M and
A5: b1 in M and
A6: b3 in M and
A7: a2 in N and
A8: a4 in N and
A9: b2 in N and
A10: b4 in N and
A11: not a4 in M and
A12: not a2 in M and
A13: not b2 in M and
A14: not b4 in M and
A15: not a1 in N and
A16: not a3 in N and
A17: not b1 in N and
not b3 in N and
A18: a3,a2 // b3,b2 and
A19: a2,a1 // b2,b1 and
A20: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4
reconsider M9 = M, N9 = N as Subset of (Af X) by ANALMETR:42;
N is being_line by A2, ANALMETR:44;
then A21: N9 is being_line by ANALMETR:43;
reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of (Af X) by ANALMETR:35;
M is being_line by A2, ANALMETR:44;
then A22: M9 is being_line by ANALMETR:43;
not M9 // N9
proof
assume M9 // N9 ; ::_thesis: contradiction
then M // N by ANALMETR:46;
hence contradiction by A2, ANALMETR:52; ::_thesis: verum
end;
then ex o9 being Element of (Af X) st
( o9 in M9 & o9 in N9 ) by A22, A21, AFF_1:58;
then consider o being Element of X such that
A23: o in M and
A24: o in N ;
reconsider o9 = o as Element of (Af X) by ANALMETR:35;
A25: now__::_thesis:_(_b2_<>_b4_implies_a3,a4_//_b3,b4_)
assume A26: b2 <> b4 ; ::_thesis: a3,a4 // b3,b4
A27: now__::_thesis:_(_b1_<>_b3_implies_a3,a4_//_b3,b4_)
consider e19 being Element of (Af X) such that
A28: o9 <> e19 and
A29: e19 in M9 by A22, AFF_1:20;
reconsider e1 = e19 as Element of X by ANALMETR:35;
ex d49 being Element of (Af X) st
( o9 <> d49 & d49 in N9 ) by A21, AFF_1:20;
then consider d4 being Element of X such that
A30: d4 in N and
A31: d4 <> o ;
reconsider d49 = d4 as Element of (Af X) by ANALMETR:35;
consider e2 being Element of X such that
A32: a1,a4 _|_ d4,e2 and
A33: e2 <> d4 by ANALMETR:39;
reconsider e29 = e2 as Element of (Af X) by ANALMETR:35;
assume A34: b1 <> b3 ; ::_thesis: a3,a4 // b3,b4
not o9,e19 // d49,e29
proof
A35: a49 <> a29
proof
assume a49 = a29 ; ::_thesis: contradiction
then a2,a1 // b1,b4 by A20, ANALMETR:59;
then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def_10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; ::_thesis: verum
end;
A36: a1 <> a3
proof
assume a1 = a3 ; ::_thesis: contradiction
then a3,a2 // b2,b1 by A19, ANALMETR:59;
then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;
then b2,b3 // b2,b1 by ANALMETR:59;
then LIN b2,b3,b1 by ANALMETR:def_10;
then LIN b29,b39,b19 by ANALMETR:40;
then LIN b19,b39,b29 by AFF_1:6;
hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; ::_thesis: verum
end;
assume o9,e19 // d49,e29 ; ::_thesis: contradiction
then o,e1 // d4,e2 by ANALMETR:36;
then A37: o,e1 _|_ a1,a4 by A32, A33, ANALMETR:62;
o9,e19 // a19,a39 by A3, A4, A22, A23, A29, AFF_1:39, AFF_1:41;
then o,e1 // a1,a3 by ANALMETR:36;
then A38: a1,a3 _|_ a1,a4 by A28, A37, ANALMETR:62;
a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;
then a1,a4 // a2,a4 by A38, A36, ANALMETR:63;
then a4,a2 // a4,a1 by ANALMETR:59;
then LIN a4,a2,a1 by ANALMETR:def_10;
then LIN a49,a29,a19 by ANALMETR:40;
hence contradiction by A7, A8, A15, A21, A35, AFF_1:25; ::_thesis: verum
end;
then consider d19 being Element of (Af X) such that
A39: LIN o9,e19,d19 and
A40: LIN d49,e29,d19 by AFF_1:60;
reconsider d1 = d19 as Element of X by ANALMETR:35;
consider e19 being Element of (Af X) such that
A41: o9 <> e19 and
A42: e19 in N9 by A21, AFF_1:20;
A43: d1 in M by A22, A23, A28, A29, A39, AFF_1:25;
LIN d4,e2,d1 by A40, ANALMETR:40;
then d4,e2 // d4,d1 by ANALMETR:def_10;
then A44: d1,d4 // d4,e2 by ANALMETR:59;
then a1,a4 _|_ d1,d4 by A32, A33, ANALMETR:62;
then A45: b1,b4 _|_ d1,d4 by A3, A11, A20, ANALMETR:62;
reconsider e1 = e19 as Element of X by ANALMETR:35;
consider e2 being Element of X such that
A46: a2,a1 _|_ d1,e2 and
A47: e2 <> d1 by ANALMETR:39;
reconsider e29 = e2 as Element of (Af X) by ANALMETR:35;
not o9,e19 // e29,d19
proof
A48: a19 <> a39
proof
assume a19 = a39 ; ::_thesis: contradiction
then a3,a2 // b2,b1 by A19, ANALMETR:59;
then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;
then b2,b3 // b2,b1 by ANALMETR:59;
then LIN b2,b3,b1 by ANALMETR:def_10;
then LIN b29,b39,b19 by ANALMETR:40;
then LIN b19,b39,b29 by AFF_1:6;
hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; ::_thesis: verum
end;
o9,e19 // a29,a49 by A7, A8, A21, A24, A42, AFF_1:39, AFF_1:41;
then A49: o,e1 // a2,a4 by ANALMETR:36;
A50: a2 <> a4
proof
assume a2 = a4 ; ::_thesis: contradiction
then a2,a1 // b1,b4 by A20, ANALMETR:59;
then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def_10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; ::_thesis: verum
end;
assume o9,e19 // e29,d19 ; ::_thesis: contradiction
then A51: o,e1 // e2,d1 by ANALMETR:36;
a2,a1 _|_ e2,d1 by A46, ANALMETR:61;
then o,e1 _|_ a2,a1 by A47, A51, ANALMETR:62;
then A52: a2,a1 _|_ a2,a4 by A41, A49, ANALMETR:62;
a3,a1 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;
then a3,a1 // a2,a1 by A52, A50, ANALMETR:63;
then a1,a3 // a1,a2 by ANALMETR:59;
then LIN a1,a3,a2 by ANALMETR:def_10;
then LIN a19,a39,a29 by ANALMETR:40;
hence contradiction by A3, A4, A12, A22, A48, AFF_1:25; ::_thesis: verum
end;
then consider d29 being Element of (Af X) such that
A53: LIN o9,e19,d29 and
A54: LIN e29,d19,d29 by AFF_1:60;
reconsider d2 = d29 as Element of X by ANALMETR:35;
A55: d2 in N by A21, A24, A41, A42, A53, AFF_1:25;
LIN d19,d29,e29 by A54, AFF_1:6;
then LIN d1,d2,e2 by ANALMETR:40;
then d1,d2 // d1,e2 by ANALMETR:def_10;
then A56: d2,d1 // e2,d1 by ANALMETR:59;
A57: a2,a1 _|_ e2,d1 by A46, ANALMETR:61;
then A58: a2,a1 _|_ d2,d1 by A47, A56, ANALMETR:62;
consider e19 being Element of (Af X) such that
A59: o9 <> e19 and
A60: e19 in M9 by A22, AFF_1:20;
reconsider e1 = e19 as Element of X by ANALMETR:35;
consider e2 being Element of X such that
A61: a3,a2 _|_ d2,e2 and
A62: e2 <> d2 by ANALMETR:39;
reconsider e29 = e2 as Element of (Af X) by ANALMETR:35;
not o9,e19 // e29,d29
proof
A63: a29 <> a49
proof
assume a29 = a49 ; ::_thesis: contradiction
then a2,a1 // b1,b4 by A20, ANALMETR:59;
then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;
then b1,b4 // b1,b2 by ANALMETR:59;
then LIN b1,b4,b2 by ANALMETR:def_10;
then LIN b19,b49,b29 by ANALMETR:40;
then LIN b29,b49,b19 by AFF_1:6;
hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; ::_thesis: verum
end;
assume o9,e19 // e29,d29 ; ::_thesis: contradiction
then o,e1 // e2,d2 by ANALMETR:36;
then o,e1 // d2,e2 by ANALMETR:59;
then A64: a3,a2 _|_ o,e1 by A61, A62, ANALMETR:62;
o,e1 _|_ a2,a4 by A2, A7, A8, A23, A60, ANALMETR:56;
then a3,a2 // a2,a4 by A59, A64, ANALMETR:63;
then a2,a4 // a2,a3 by ANALMETR:59;
then LIN a2,a4,a3 by ANALMETR:def_10;
then LIN a29,a49,a39 by ANALMETR:40;
hence contradiction by A7, A8, A16, A21, A63, AFF_1:25; ::_thesis: verum
end;
then consider d39 being Element of (Af X) such that
A65: LIN o9,e19,d39 and
A66: LIN e29,d29,d39 by AFF_1:60;
reconsider d3 = d39 as Element of X by ANALMETR:35;
A67: d3 in M by A22, A23, A59, A60, A65, AFF_1:25;
then A68: d3 <> d4 by A2, A22, A21, A23, A24, A30, A31, AFF_1:18;
a2,a1 _|_ d2,d1 by A47, A56, A57, ANALMETR:62;
then A69: b2,b1 _|_ d2,d1 by A3, A12, A19, ANALMETR:62;
LIN d29,d39,e29 by A66, AFF_1:6;
then LIN d2,d3,e2 by ANALMETR:40;
then d2,d3 // d2,e2 by ANALMETR:def_10;
then d3,d2 // d2,e2 by ANALMETR:59;
then A70: a3,a2 _|_ d3,d2 by A61, A62, ANALMETR:62;
then b3,b2 _|_ d3,d2 by A4, A12, A18, ANALMETR:62;
then A71: b3,b4 _|_ d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A30, A43, A55, A67, A45, A69, Def3;
a1,a4 _|_ d1,d4 by A32, A33, A44, ANALMETR:62;
then a3,a4 _|_ d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A30, A43, A55, A58, A70, A67, Def3;
hence a3,a4 // b3,b4 by A68, A71, ANALMETR:63; ::_thesis: verum
end;
now__::_thesis:_(_b1_=_b3_implies_a3,a4_//_b3,b4_)
A72: not LIN o9,a29,a19
proof
assume LIN o9,a29,a19 ; ::_thesis: contradiction
then o9,a29 // o9,a19 by AFF_1:def_1;
hence contradiction by A7, A12, A15, A21, A23, A24, AFF_1:48; ::_thesis: verum
end;
A73: LIN o9,a19,a39 by A3, A4, A22, A23, AFF_1:21;
assume A74: b1 = b3 ; ::_thesis: a3,a4 // b3,b4
then a2,a3 // b2,b1 by A18, ANALMETR:59;
then A75: a29,a39 // b29,b19 by ANALMETR:36;
a29,a19 // b29,b19 by A19, ANALMETR:36;
then a29,a19 // a29,a39 by A5, A13, A75, AFF_1:5;
hence a3,a4 // b3,b4 by A20, A74, A72, A73, AFF_1:14; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A27; ::_thesis: verum
end;
now__::_thesis:_(_b2_=_b4_implies_a3,a4_//_b3,b4_)
A76: not LIN o9,a19,a49
proof
assume LIN o9,a19,a49 ; ::_thesis: contradiction
then ex A9 being Subset of (Af X) st
( A9 is being_line & o9 in A9 & a19 in A9 & a49 in A9 ) by AFF_1:21;
hence contradiction by A3, A11, A15, A22, A23, A24, AFF_1:18; ::_thesis: verum
end;
assume A77: b2 = b4 ; ::_thesis: a3,a4 // b3,b4
b1,b2 // a1,a2 by A19, ANALMETR:59;
then a1,a4 // a1,a2 by A5, A13, A20, A77, ANALMETR:60;
then A78: a19,a49 // a19,a29 by ANALMETR:36;
LIN o9,a49,a29 by A7, A8, A21, A24, AFF_1:21;
hence a3,a4 // b3,b4 by A18, A77, A78, A76, AFF_1:14; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A25; ::_thesis: verum
end;
theorem :: CONMETR:10
for X being OrtAfPl st X is satisfying_MH2 holds
X is satisfying_OSCH
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_MH2 implies X is satisfying_OSCH )
assume A1: X is satisfying_MH2 ; ::_thesis: X is satisfying_OSCH
let a1 be Element of X; :: according to CONMETR:def_7 ::_thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let M, N be Subset of X; ::_thesis: ( M _|_ N & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )
assume that
A2: M _|_ N and
A3: a1 in M and
A4: a3 in M and
A5: b1 in M and
A6: b3 in M and
A7: a2 in N and
A8: a4 in N and
A9: b2 in N and
A10: b4 in N and
A11: not a4 in M and
A12: not a2 in M and
A13: not b2 in M and
A14: not b4 in M and
A15: not a1 in N and
A16: not a3 in N and
A17: not b1 in N and
not b3 in N and
A18: a3,a2 // b3,b2 and
A19: a2,a1 // b2,b1 and
A20: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4
reconsider M9 = M, N9 = N as Subset of (Af X) by ANALMETR:42;
N is being_line by A2, ANALMETR:44;
then A21: N9 is being_line by ANALMETR:43;
reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of (Af X) by ANALMETR:35;
M is being_line by A2, ANALMETR:44;
then A22: M9 is being_line by ANALMETR:43;
not M9 // N9
proof
assume M9 // N9 ; ::_thesis: contradiction
then M // N by ANALMETR:46;
hence contradiction by A2, ANALMETR:52; ::_thesis: verum
end;
then ex o9 being Element of (Af X) st
( o9 in M9 & o9 in N9 ) by A22, A21, AFF_1:58;
then consider o being Element of X such that
A23: o in M and
A24: o in N ;
reconsider o9 = o as Element of (Af X) by ANALMETR:35;
A25: now__::_thesis:_(_b2_<>_b4_implies_a3,a4_//_b3,b4_)
assume A26: b2 <> b4 ; ::_thesis: a3,a4 // b3,b4
A27: now__::_thesis:_(_b1_<>_b3_implies_a3,a4_//_b3,b4_)
ex d39 being Element of (Af X) st
( o9 <> d39 & d39 in N9 ) by A21, AFF_1:20;
then consider d3 being Element of X such that
A28: d3 in N and
A29: d3 <> o ;
reconsider d39 = d3 as Element of (Af X) by ANALMETR:35;
consider e2 being Element of X such that
A30: a3,a2 _|_ d3,e2 and
A31: d3 <> e2 by ANALMETR:def_9;
consider e1 being Element of X such that
A32: a3,a1 // a3,e1 and
A33: a3 <> e1 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
assume A34: b1 <> b3 ; ::_thesis: a3,a4 // b3,b4
A35: ( a1 <> a3 & a2 <> a4 )
proof
assume ( a1 = a3 or a2 = a4 ) ; ::_thesis: contradiction
then ( a2,a1 // b3,b2 or a1,a4 // b2,b1 ) by A18, A19, ANALMETR:59;
then ( b3,b2 // b2,b1 or b2,b1 // b1,b4 ) by A3, A11, A12, A19, A20, ANALMETR:60;
then ( b2,b3 // b2,b1 or b1,b2 // b1,b4 ) by ANALMETR:59;
then ( LIN b2,b3,b1 or LIN b1,b2,b4 ) by ANALMETR:def_10;
then ( LIN b29,b39,b19 or LIN b19,b29,b49 ) by ANALMETR:40;
then ( LIN b19,b39,b29 or LIN b29,b49,b19 ) by AFF_1:6;
hence contradiction by A5, A6, A9, A10, A13, A17, A22, A21, A26, A34, AFF_1:25; ::_thesis: verum
end;
not a39,e19 // d39,e29
proof
assume a39,e19 // d39,e29 ; ::_thesis: contradiction
then a3,e1 // d3,e2 by ANALMETR:36;
then a3,a1 // d3,e2 by A32, A33, ANALMETR:60;
then A36: a3,a2 _|_ a3,a1 by A30, A31, ANALMETR:62;
a3,a1 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;
then a3,a2 // a2,a4 by A35, A36, ANALMETR:63;
then a2,a4 // a2,a3 by ANALMETR:59;
then LIN a2,a4,a3 by ANALMETR:def_10;
then LIN a29,a49,a39 by ANALMETR:40;
hence contradiction by A7, A8, A16, A21, A35, AFF_1:25; ::_thesis: verum
end;
then consider d29 being Element of (Af X) such that
A37: LIN a39,e19,d29 and
A38: LIN d39,e29,d29 by AFF_1:60;
reconsider d2 = d29 as Element of X by ANALMETR:35;
LIN d3,e2,d2 by A38, ANALMETR:40;
then d3,e2 // d3,d2 by ANALMETR:def_10;
then A39: a3,a2 _|_ d3,d2 by A30, A31, ANALMETR:62;
LIN a3,e1,d2 by A37, ANALMETR:40;
then a3,e1 // a3,d2 by ANALMETR:def_10;
then a3,a1 // a3,d2 by A32, A33, ANALMETR:60;
then LIN a3,a1,d2 by ANALMETR:def_10;
then LIN a39,a19,d29 by ANALMETR:40;
then consider d2 being Element of X such that
A40: d2 in M and
A41: a3,a2 _|_ d3,d2 by A3, A4, A22, A35, A39, AFF_1:25;
reconsider d29 = d2 as Element of (Af X) by ANALMETR:35;
consider e1 being Element of X such that
A42: a2,a4 // a2,e1 and
A43: a2 <> e1 by ANALMETR:39;
consider e2 being Element of X such that
A44: a2,a1 _|_ d2,e2 and
A45: d2 <> e2 by ANALMETR:def_9;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
not a29,e19 // d29,e29
proof
assume a29,e19 // d29,e29 ; ::_thesis: contradiction
then a2,e1 // d2,e2 by ANALMETR:36;
then a2,a4 // d2,e2 by A42, A43, ANALMETR:60;
then A46: a2,a4 _|_ a2,a1 by A44, A45, ANALMETR:62;
a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;
then a1,a3 // a2,a1 by A35, A46, ANALMETR:63;
then a1,a3 // a1,a2 by ANALMETR:59;
then LIN a1,a3,a2 by ANALMETR:def_10;
then LIN a19,a39,a29 by ANALMETR:40;
hence contradiction by A3, A4, A12, A22, A35, AFF_1:25; ::_thesis: verum
end;
then consider d19 being Element of (Af X) such that
A47: LIN a29,e19,d19 and
A48: LIN d29,e29,d19 by AFF_1:60;
reconsider d1 = d19 as Element of X by ANALMETR:35;
A49: b3,b2 _|_ d3,d2 by A4, A12, A18, A41, ANALMETR:62;
LIN a2,e1,d1 by A47, ANALMETR:40;
then a2,e1 // a2,d1 by ANALMETR:def_10;
then a2,a4 // a2,d1 by A42, A43, ANALMETR:60;
then LIN a2,a4,d1 by ANALMETR:def_10;
then LIN a29,a49,d19 by ANALMETR:40;
then A50: d1 in N by A7, A8, A21, A35, AFF_1:25;
LIN d2,e2,d1 by A48, ANALMETR:40;
then d2,e2 // d2,d1 by ANALMETR:def_10;
then A51: a2,a1 _|_ d2,d1 by A44, A45, ANALMETR:62;
then A52: b2,b1 _|_ d2,d1 by A3, A12, A19, ANALMETR:62;
consider e2 being Element of X such that
A53: a1,a4 _|_ d1,e2 and
A54: d1 <> e2 by ANALMETR:39;
consider e1 being Element of X such that
A55: a1,a3 // a1,e1 and
A56: a1 <> e1 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
not a19,e19 // d19,e29
proof
assume a19,e19 // d19,e29 ; ::_thesis: contradiction
then a1,e1 // d1,e2 by ANALMETR:36;
then a1,a3 // d1,e2 by A55, A56, ANALMETR:60;
then A57: a1,a3 _|_ a1,a4 by A53, A54, ANALMETR:62;
a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;
then a2,a4 // a1,a4 by A35, A57, ANALMETR:63;
then a4,a2 // a4,a1 by ANALMETR:59;
then LIN a4,a2,a1 by ANALMETR:def_10;
then LIN a49,a29,a19 by ANALMETR:40;
hence contradiction by A7, A8, A15, A21, A35, AFF_1:25; ::_thesis: verum
end;
then consider d49 being Element of (Af X) such that
A58: LIN a19,e19,d49 and
A59: LIN d19,e29,d49 by AFF_1:60;
reconsider d4 = d49 as Element of X by ANALMETR:35;
LIN a1,e1,d4 by A58, ANALMETR:40;
then a1,e1 // a1,d4 by ANALMETR:def_10;
then a1,a3 // a1,d4 by A55, A56, ANALMETR:60;
then LIN a1,a3,d4 by ANALMETR:def_10;
then LIN a19,a39,d49 by ANALMETR:40;
then A60: d4 in M by A3, A4, A22, A35, AFF_1:25;
then A61: d3 <> d4 by A2, A22, A21, A23, A24, A28, A29, AFF_1:18;
LIN d1,e2,d4 by A59, ANALMETR:40;
then d1,e2 // d1,d4 by ANALMETR:def_10;
then A62: a1,a4 _|_ d1,d4 by A53, A54, ANALMETR:62;
then b1,b4 _|_ d1,d4 by A3, A11, A20, ANALMETR:62;
then A63: b3,b4 _|_ d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A28, A40, A50, A60, A49, A52, Def4;
a3,a4 _|_ d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A28, A40, A41, A50, A51, A60, A62, Def4;
hence a3,a4 // b3,b4 by A63, A61, ANALMETR:63; ::_thesis: verum
end;
now__::_thesis:_(_b1_=_b3_implies_a3,a4_//_b3,b4_)
o9,a19 // o9,a39 by A3, A4, A22, A23, AFF_1:39, AFF_1:41;
then A64: LIN o9,a19,a39 by AFF_1:def_1;
assume A65: b1 = b3 ; ::_thesis: a3,a4 // b3,b4
then a2,a1 // b3,b2 by A19, ANALMETR:59;
then a2,a1 // a3,a2 by A6, A13, A18, ANALMETR:60;
then a2,a1 // a2,a3 by ANALMETR:59;
then a29,a19 // a29,a39 by ANALMETR:36;
hence a3,a4 // b3,b4 by A7, A12, A15, A20, A21, A23, A24, A65, A64, AFF_1:14, AFF_1:25; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A27; ::_thesis: verum
end;
now__::_thesis:_(_b2_=_b4_implies_a3,a4_//_b3,b4_)
o9,a29 // o9,a49 by A7, A8, A21, A24, AFF_1:39, AFF_1:41;
then A66: LIN o9,a29,a49 by AFF_1:def_1;
assume A67: b2 = b4 ; ::_thesis: a3,a4 // b3,b4
then a1,a4 // b2,b1 by A20, ANALMETR:59;
then a2,a1 // a1,a4 by A5, A13, A19, ANALMETR:60;
then a1,a2 // a1,a4 by ANALMETR:59;
then a19,a29 // a19,a49 by ANALMETR:36;
hence a3,a4 // b3,b4 by A3, A12, A15, A18, A22, A23, A24, A67, A66, AFF_1:14, AFF_1:25; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A25; ::_thesis: verum
end;
theorem :: CONMETR:11
for X being OrtAfPl st X is satisfying_AH holds
X is satisfying_TDES
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_AH implies X is satisfying_TDES )
assume A1: X is satisfying_AH ; ::_thesis: X is satisfying_TDES
let o be Element of X; :: according to CONMETR:def_5 ::_thesis: for a, a1, b, b1, c, c1 being Element of X st o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 holds
a,c // a1,c1
let a, a1, b, b1, c, c1 be Element of X; ::_thesis: ( o <> a & o <> a1 & o <> b & o <> b1 & o <> c & o <> c1 & not LIN b,b1,a & not LIN b,b1,c & LIN o,a,a1 & LIN o,b,b1 & LIN o,c,c1 & a,b // a1,b1 & a,b // o,c & b,c // b1,c1 implies a,c // a1,c1 )
assume that
A2: o <> a and
A3: o <> a1 and
A4: o <> b and
A5: o <> b1 and
A6: o <> c and
A7: o <> c1 and
A8: not LIN b,b1,a and
A9: not LIN b,b1,c and
A10: LIN o,a,a1 and
A11: LIN o,b,b1 and
A12: LIN o,c,c1 and
A13: a,b // a1,b1 and
A14: a,b // o,c and
A15: b,c // b1,c1 ; ::_thesis: a,c // a1,c1
consider e1 being Element of X such that
A16: o,b _|_ o,e1 and
A17: o <> e1 by ANALMETR:def_9;
consider c2 being Element of X such that
A18: o,c _|_ o,c2 and
A19: o <> c2 by ANALMETR:def_9;
consider e2 being Element of X such that
A20: b,c _|_ c2,e2 and
A21: c2 <> e2 by ANALMETR:def_9;
reconsider o9 = o, a9 = a, a19 = a1, b9 = b, b19 = b1, c9 = c, c19 = c1, c29 = c2, e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
A22: b1 <> a1
proof
assume b1 = a1 ; ::_thesis: contradiction
then LIN o9,b9,a19 by A11, ANALMETR:40;
then o9,b9 // o9,a19 by AFF_1:def_1;
then o9,a19 // o9,b9 by AFF_1:4;
then A23: o,a1 // o,b by ANALMETR:36;
o,a // o,a1 by A10, ANALMETR:def_10;
then o9,a9 // o9,a19 by ANALMETR:36;
then o9,a19 // o9,a9 by AFF_1:4;
then o,a1 // o,a by ANALMETR:36;
then o,a // o,b by A3, A23, ANALMETR:60;
then LIN o,a,b by ANALMETR:def_10;
then A24: LIN o9,a9,b9 by ANALMETR:40;
then LIN b9,o9,a9 by AFF_1:6;
then b9,o9 // b9,a9 by AFF_1:def_1;
then o9,b9 // a9,b9 by AFF_1:4;
then A25: o,b // a,b by ANALMETR:36;
A26: a9 <> b9
proof
assume a9 = b9 ; ::_thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8, ANALMETR:40; ::_thesis: verum
end;
o,b // o,b1 by A11, ANALMETR:def_10;
then a,b // o,b1 by A4, A25, ANALMETR:60;
then A27: a9,b9 // o9,b19 by ANALMETR:36;
LIN a9,b9,o9 by A24, AFF_1:6;
then LIN a9,b9,b19 by A27, A26, AFF_1:9;
then LIN b9,b19,a9 by AFF_1:6;
hence contradiction by A8, ANALMETR:40; ::_thesis: verum
end;
A28: now__::_thesis:_(_not_LIN_a,b,c_implies_a,c_//_a1,c1_)
not o9,e19 // c29,e29
proof
assume o9,e19 // c29,e29 ; ::_thesis: contradiction
then o,e1 // c2,e2 by ANALMETR:36;
then c2,e2 _|_ o,b by A16, A17, ANALMETR:62;
then c2,e2 _|_ b,o by ANALMETR:61;
then b,c // b,o by A20, A21, ANALMETR:63;
then LIN b,c,o by ANALMETR:def_10;
then LIN b9,c9,o9 by ANALMETR:40;
then LIN b9,o9,c9 by AFF_1:6;
then LIN b,o,c by ANALMETR:40;
then A29: b,o // b,c by ANALMETR:def_10;
LIN o9,b9,b19 by A11, ANALMETR:40;
then LIN b9,o9,b19 by AFF_1:6;
then LIN b,o,b1 by ANALMETR:40;
then b,o // b,b1 by ANALMETR:def_10;
then b,b1 // b,c by A4, A29, ANALMETR:60;
hence contradiction by A9, ANALMETR:def_10; ::_thesis: verum
end;
then consider b29 being Element of (Af X) such that
A30: LIN o9,e19,b29 and
A31: LIN c29,e29,b29 by AFF_1:60;
reconsider b2 = b29 as Element of X by ANALMETR:35;
LIN o,e1,b2 by A30, ANALMETR:40;
then o,e1 // o,b2 by ANALMETR:def_10;
then A32: o,b _|_ o,b2 by A16, A17, ANALMETR:62;
o,b // o,b1 by A11, ANALMETR:def_10;
then A33: o,b1 _|_ o,b2 by A4, A32, ANALMETR:62;
assume A34: not LIN a,b,c ; ::_thesis: a,c // a1,c1
A35: b <> a
proof
assume b = a ; ::_thesis: contradiction
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34, ANALMETR:40; ::_thesis: verum
end;
A36: not o,c // o,b
proof
assume o,c // o,b ; ::_thesis: contradiction
then LIN o,c,b by ANALMETR:def_10;
then LIN o9,c9,b9 by ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then c9,o9 // c9,b9 by AFF_1:def_1;
then o9,c9 // b9,c9 by AFF_1:4;
then A37: o,c // b,c by ANALMETR:36;
a9,b9 // o9,c9 by A14, ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then o,c // b,a by ANALMETR:36;
then b,a // b,c by A6, A37, ANALMETR:60;
then LIN b,a,c by ANALMETR:def_10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A34, ANALMETR:40; ::_thesis: verum
end;
A38: not o,a // o,c
proof
assume o,a // o,c ; ::_thesis: contradiction
then LIN o,a,c by ANALMETR:def_10;
then LIN o9,a9,c9 by ANALMETR:40;
then LIN c9,o9,a9 by AFF_1:6;
then LIN c,o,a by ANALMETR:40;
then A39: c,o // c,a by ANALMETR:def_10;
a9,b9 // o9,c9 by A14, ANALMETR:36;
then c9,o9 // a9,b9 by AFF_1:4;
then c,o // a,b by ANALMETR:36;
then a,b // c,a by A6, A39, ANALMETR:60;
then a9,b9 // c9,a9 by ANALMETR:36;
then a9,b9 // a9,c9 by AFF_1:4;
then a,b // a,c by ANALMETR:36;
hence contradiction by A34, ANALMETR:def_10; ::_thesis: verum
end;
LIN c2,e2,b2 by A31, ANALMETR:40;
then c2,e2 // c2,b2 by ANALMETR:def_10;
then A40: b,c _|_ c2,b2 by A20, A21, ANALMETR:62;
consider e1 being Element of X such that
A41: o,a _|_ o,e1 and
A42: o <> e1 by ANALMETR:def_9;
consider e2 being Element of X such that
A43: a,c _|_ c2,e2 and
A44: c2 <> e2 by ANALMETR:def_9;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
not o9,e19 // c29,e29
proof
assume o9,e19 // c29,e29 ; ::_thesis: contradiction
then o,e1 // c2,e2 by ANALMETR:36;
then c2,e2 _|_ o,a by A41, A42, ANALMETR:62;
then a,c // o,a by A43, A44, ANALMETR:63;
then a9,c9 // o9,a9 by ANALMETR:36;
then a9,c9 // a9,o9 by AFF_1:4;
then LIN a9,c9,o9 by AFF_1:def_1;
then LIN c9,o9,a9 by AFF_1:6;
then LIN c,o,a by ANALMETR:40;
then A45: c,o // c,a by ANALMETR:def_10;
a9,b9 // o9,c9 by A14, ANALMETR:36;
then c9,o9 // a9,b9 by AFF_1:4;
then c,o // a,b by ANALMETR:36;
then a,b // c,a by A6, A45, ANALMETR:60;
then a9,b9 // c9,a9 by ANALMETR:36;
then a9,b9 // a9,c9 by AFF_1:4;
then a,b // a,c by ANALMETR:36;
hence contradiction by A34, ANALMETR:def_10; ::_thesis: verum
end;
then consider a29 being Element of (Af X) such that
A46: LIN o9,e19,a29 and
A47: LIN c29,e29,a29 by AFF_1:60;
reconsider a2 = a29 as Element of X by ANALMETR:35;
LIN o,e1,a2 by A46, ANALMETR:40;
then o,e1 // o,a2 by ANALMETR:def_10;
then A48: o,a _|_ o,a2 by A41, A42, ANALMETR:62;
A49: c2 <> a2
proof
assume c2 = a2 ; ::_thesis: contradiction
then o,c // o,a by A18, A19, A48, ANALMETR:63;
then LIN o,c,a by ANALMETR:def_10;
then LIN o9,c9,a9 by ANALMETR:40;
then LIN c9,a9,o9 by AFF_1:6;
then c9,a9 // c9,o9 by AFF_1:def_1;
then o9,c9 // a9,c9 by AFF_1:4;
then o,c // a,c by ANALMETR:36;
then a,b // a,c by A6, A14, ANALMETR:60;
hence contradiction by A34, ANALMETR:def_10; ::_thesis: verum
end;
LIN c2,e2,a2 by A47, ANALMETR:40;
then c2,e2 // c2,a2 by ANALMETR:def_10;
then a,c _|_ c2,a2 by A43, A44, ANALMETR:62;
then A50: c,a _|_ c2,a2 by ANALMETR:61;
A51: not LIN o9,b29,a29
proof
A52: o <> b2
proof
a9,b9 // o9,c9 by A14, ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then A53: o,c // b,a by ANALMETR:36;
assume o = b2 ; ::_thesis: contradiction
then o,c2 _|_ b,c by A40, ANALMETR:61;
then o,c // b,c by A18, A19, ANALMETR:63;
then b,a // b,c by A6, A53, ANALMETR:60;
then LIN b,a,c by ANALMETR:def_10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A34, ANALMETR:40; ::_thesis: verum
end;
A54: o <> a2
proof
assume A55: o = a2 ; ::_thesis: contradiction
c2,o _|_ o,c by A18, ANALMETR:61;
then o,c // c,a by A19, A50, A55, ANALMETR:63;
then a,b // c,a by A6, A14, ANALMETR:60;
then a9,b9 // c9,a9 by ANALMETR:36;
then a9,b9 // a9,c9 by AFF_1:4;
then a,b // a,c by ANALMETR:36;
hence contradiction by A34, ANALMETR:def_10; ::_thesis: verum
end;
assume LIN o9,b29,a29 ; ::_thesis: contradiction
then LIN o,b2,a2 by ANALMETR:40;
then o,b2 // o,a2 by ANALMETR:def_10;
then o,a2 _|_ o,b by A32, A52, ANALMETR:62;
then o,a // o,b by A48, A54, ANALMETR:63;
then LIN o,a,b by ANALMETR:def_10;
then LIN o9,a9,b9 by ANALMETR:40;
then A56: LIN a9,b9,o9 by AFF_1:6;
A57: a9 <> b9
proof
assume a9 = b9 ; ::_thesis: contradiction
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34, ANALMETR:40; ::_thesis: verum
end;
a9,b9 // o9,c9 by A14, ANALMETR:36;
then LIN a9,b9,c9 by A56, A57, AFF_1:9;
hence contradiction by A34, ANALMETR:40; ::_thesis: verum
end;
consider e1 being Element of X such that
A58: o,a1 _|_ o,e1 and
A59: o <> e1 by ANALMETR:def_9;
consider e2 being Element of X such that
A60: a1,c1 _|_ c2,e2 and
A61: c2 <> e2 by ANALMETR:def_9;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
not o9,e19 // c29,e29
proof
assume o9,e19 // c29,e29 ; ::_thesis: contradiction
then o,e1 // c2,e2 by ANALMETR:36;
then c2,e2 _|_ o,a1 by A58, A59, ANALMETR:62;
then a1,c1 // o,a1 by A60, A61, ANALMETR:63;
then a19,c19 // o9,a19 by ANALMETR:36;
then a19,c19 // a19,o9 by AFF_1:4;
then LIN a19,c19,o9 by AFF_1:def_1;
then LIN o9,c19,a19 by AFF_1:6;
then o9,c19 // o9,a19 by AFF_1:def_1;
then A62: o,c1 // o,a1 by ANALMETR:36;
LIN o9,a9,a19 by A10, ANALMETR:40;
then o9,a9 // o9,a19 by AFF_1:def_1;
then o9,a19 // o9,a9 by AFF_1:4;
then A63: o,a1 // o,a by ANALMETR:36;
LIN o9,c9,c19 by A12, ANALMETR:40;
then o9,c9 // o9,c19 by AFF_1:def_1;
then o9,c19 // o9,c9 by AFF_1:4;
then o,c1 // o,c by ANALMETR:36;
then o,a1 // o,c by A7, A62, ANALMETR:60;
then o,a // o,c by A3, A63, ANALMETR:60;
then LIN o,a,c by ANALMETR:def_10;
then LIN o9,a9,c9 by ANALMETR:40;
then LIN c9,o9,a9 by AFF_1:6;
then c9,o9 // c9,a9 by AFF_1:def_1;
then o9,c9 // a9,c9 by AFF_1:4;
then o,c // a,c by ANALMETR:36;
then a,b // a,c by A6, A14, ANALMETR:60;
hence contradiction by A34, ANALMETR:def_10; ::_thesis: verum
end;
then consider a39 being Element of (Af X) such that
A64: LIN o9,e19,a39 and
A65: LIN c29,e29,a39 by AFF_1:60;
reconsider a3 = a39 as Element of X by ANALMETR:35;
LIN o,e1,a3 by A64, ANALMETR:40;
then o,e1 // o,a3 by ANALMETR:def_10;
then A66: o,a1 _|_ o,a3 by A58, A59, ANALMETR:62;
b <> c
proof
assume b = c ; ::_thesis: contradiction
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A34, ANALMETR:40; ::_thesis: verum
end;
then c2,b2 _|_ b1,c1 by A15, A40, ANALMETR:62;
then A67: c1,b1 _|_ c2,b2 by ANALMETR:61;
A68: not o,a1 // o,c1
proof
o,a // o,a1 by A10, ANALMETR:def_10;
then o9,a9 // o9,a19 by ANALMETR:36;
then o9,a19 // o9,a9 by AFF_1:4;
then A69: o,a1 // o,a by ANALMETR:36;
assume o,a1 // o,c1 ; ::_thesis: contradiction
then o9,a19 // o9,c19 by ANALMETR:36;
then o9,c19 // o9,a19 by AFF_1:4;
then A70: o,c1 // o,a1 by ANALMETR:36;
o,c // o,c1 by A12, ANALMETR:def_10;
then o9,c9 // o9,c19 by ANALMETR:36;
then o9,c19 // o9,c9 by AFF_1:4;
then o,c1 // o,c by ANALMETR:36;
then o,a1 // o,c by A7, A70, ANALMETR:60;
then o,a // o,c by A3, A69, ANALMETR:60;
then LIN o,a,c by ANALMETR:def_10;
then LIN o9,a9,c9 by ANALMETR:40;
then LIN c9,a9,o9 by AFF_1:6;
then c9,a9 // c9,o9 by AFF_1:def_1;
then o9,c9 // a9,c9 by AFF_1:4;
then o,c // a,c by ANALMETR:36;
then a,b // a,c by A6, A14, ANALMETR:60;
hence contradiction by A34, ANALMETR:def_10; ::_thesis: verum
end;
a9,b9 // o9,c9 by A14, ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then A71: o,c // b,a by ANALMETR:36;
A72: not o,c1 // o,b1
proof
o,b // o,b1 by A11, ANALMETR:def_10;
then o9,b9 // o9,b19 by ANALMETR:36;
then o9,b19 // o9,b9 by AFF_1:4;
then A73: o,b1 // o,b by ANALMETR:36;
o,c // o,c1 by A12, ANALMETR:def_10;
then o9,c9 // o9,c19 by ANALMETR:36;
then o9,c19 // o9,c9 by AFF_1:4;
then A74: o,c1 // o,c by ANALMETR:36;
assume o,c1 // o,b1 ; ::_thesis: contradiction
then o,b1 // o,c by A7, A74, ANALMETR:60;
then o,b // o,c by A5, A73, ANALMETR:60;
then LIN o,b,c by ANALMETR:def_10;
then LIN o9,b9,c9 by ANALMETR:40;
then LIN c9,o9,b9 by AFF_1:6;
then c9,o9 // c9,b9 by AFF_1:def_1;
then o9,c9 // b9,c9 by AFF_1:4;
then A75: o,c // b,c by ANALMETR:36;
a9,b9 // o9,c9 by A14, ANALMETR:36;
then o9,c9 // b9,a9 by AFF_1:4;
then o,c // b,a by ANALMETR:36;
then b,a // b,c by A6, A75, ANALMETR:60;
then LIN b,a,c by ANALMETR:def_10;
then LIN b9,a9,c9 by ANALMETR:40;
then LIN a9,b9,c9 by AFF_1:6;
hence contradiction by A34, ANALMETR:40; ::_thesis: verum
end;
a <> b
proof
assume a = b ; ::_thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8, ANALMETR:40; ::_thesis: verum
end;
then o,c // a1,b1 by A13, A14, ANALMETR:60;
then o9,c9 // a19,b19 by ANALMETR:36;
then o9,c9 // b19,a19 by AFF_1:4;
then A76: o,c // b1,a1 by ANALMETR:36;
o,c // o,c1 by A12, ANALMETR:def_10;
then A77: o,c1 // b1,a1 by A6, A76, ANALMETR:60;
o,c // o,c1 by A12, ANALMETR:def_10;
then A78: o,c1 _|_ o,c2 by A6, A18, ANALMETR:62;
c,b _|_ c2,b2 by A40, ANALMETR:61;
then b,a _|_ b2,a2 by A1, A18, A32, A48, A71, A50, A38, A36, CONAFFM:def_2;
then b2,a2 _|_ a,b by ANALMETR:61;
then b2,a2 _|_ a1,b1 by A13, A35, ANALMETR:62;
then A79: b1,a1 _|_ b2,a2 by ANALMETR:61;
o,a // o,a1 by A10, ANALMETR:def_10;
then o,a1 _|_ o,a2 by A2, A48, ANALMETR:62;
then o,a2 // o,a3 by A3, A66, ANALMETR:63;
then LIN o,a2,a3 by ANALMETR:def_10;
then A80: LIN o9,a29,a39 by ANALMETR:40;
LIN c2,e2,a3 by A65, ANALMETR:40;
then c2,e2 // c2,a3 by ANALMETR:def_10;
then A81: a1,c1 _|_ c2,a3 by A60, A61, ANALMETR:62;
then c1,a1 _|_ c2,a3 by ANALMETR:61;
then b1,a1 _|_ b2,a3 by A1, A66, A78, A33, A67, A77, A68, A72, CONAFFM:def_2;
then b2,a3 // b2,a2 by A22, A79, ANALMETR:63;
then b29,a39 // b29,a29 by ANALMETR:36;
then b29,a29 // b29,a39 by AFF_1:4;
then a29 = a39 by A51, A80, AFF_1:14;
then c,a // a1,c1 by A50, A81, A49, ANALMETR:63;
then c9,a9 // a19,c19 by ANALMETR:36;
then a9,c9 // a19,c19 by AFF_1:4;
hence a,c // a1,c1 by ANALMETR:36; ::_thesis: verum
end;
now__::_thesis:_(_LIN_a,b,c_implies_a,c_//_a1,c1_)
assume A82: LIN a,b,c ; ::_thesis: a,c // a1,c1
then A83: LIN a9,b9,c9 by ANALMETR:40;
A84: a <> b
proof
assume a = b ; ::_thesis: contradiction
then LIN b9,b19,a9 by AFF_1:7;
hence contradiction by A8, ANALMETR:40; ::_thesis: verum
end;
A85: now__::_thesis:_(_a1,c1_//_a,b_implies_a,c_//_a1,c1_)
assume a1,c1 // a,b ; ::_thesis: a,c // a1,c1
then a19,c19 // a9,b9 by ANALMETR:36;
then a9,b9 // a19,c19 by AFF_1:4;
then A86: a,b // a1,c1 by ANALMETR:36;
a,b // a,c by A82, ANALMETR:def_10;
hence a,c // a1,c1 by A84, A86, ANALMETR:60; ::_thesis: verum
end;
A87: b <> c
proof
assume b = c ; ::_thesis: contradiction
then LIN b9,b19,c9 by AFF_1:7;
hence contradiction by A9, ANALMETR:40; ::_thesis: verum
end;
A88: now__::_thesis:_(_a1_=_b1_implies_a,c_//_a1,c1_)
LIN c9,b9,a9 by A83, AFF_1:6;
then c9,b9 // c9,a9 by AFF_1:def_1;
then b9,c9 // a9,c9 by AFF_1:4;
then A89: b,c // a,c by ANALMETR:36;
assume a1 = b1 ; ::_thesis: a,c // a1,c1
hence a,c // a1,c1 by A15, A87, A89, ANALMETR:60; ::_thesis: verum
end;
LIN b9,a9,c9 by A83, AFF_1:6;
then b9,a9 // b9,c9 by AFF_1:def_1;
then a9,b9 // b9,c9 by AFF_1:4;
then a,b // b,c by ANALMETR:36;
then b,c // a1,b1 by A13, A84, ANALMETR:60;
then b1,c1 // a1,b1 by A15, A87, ANALMETR:60;
then b19,c19 // a19,b19 by ANALMETR:36;
then b19,a19 // b19,c19 by AFF_1:4;
then LIN b19,a19,c19 by AFF_1:def_1;
then LIN a19,b19,c19 by AFF_1:6;
then LIN a1,b1,c1 by ANALMETR:40;
then A90: a1,b1 // a1,c1 by ANALMETR:def_10;
a9,b9 // a19,b19 by A13, ANALMETR:36;
then a19,b19 // a9,b9 by AFF_1:4;
then a1,b1 // a,b by ANALMETR:36;
hence a,c // a1,c1 by A90, A85, A88, ANALMETR:60; ::_thesis: verum
end;
hence a,c // a1,c1 by A28; ::_thesis: verum
end;
theorem :: CONMETR:12
for X being OrtAfPl st X is satisfying_OSCH & X is satisfying_TDES holds
X is satisfying_SCH
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH )
assume that
A1: X is satisfying_OSCH and
A2: X is satisfying_TDES ; ::_thesis: X is satisfying_SCH
let a1 be Element of X; :: according to CONMETR:def_6 ::_thesis: for a2, a3, a4, b1, b2, b3, b4 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let a2, a3, a4, b1, b2, b3, b4 be Element of X; ::_thesis: for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds
a3,a4 // b3,b4
let M, N be Subset of X; ::_thesis: ( M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )
assume that
A3: M is being_line and
A4: N is being_line and
A5: a1 in M and
A6: a3 in M and
A7: b1 in M and
A8: b3 in M and
A9: a2 in N and
A10: a4 in N and
A11: b2 in N and
A12: b4 in N and
A13: not a4 in M and
A14: not a2 in M and
A15: not b2 in M and
A16: not b4 in M and
A17: not a1 in N and
A18: not a3 in N and
A19: not b1 in N and
A20: not b3 in N and
A21: a3,a2 // b3,b2 and
A22: a2,a1 // b2,b1 and
A23: a1,a4 // b1,b4 ; ::_thesis: a3,a4 // b3,b4
reconsider a19 = a1, a29 = a2, a39 = a3, a49 = a4, b19 = b1, b29 = b2, b39 = b3, b49 = b4 as Element of (Af X) by ANALMETR:35;
reconsider M9 = M, N9 = N as Subset of (Af X) by ANALMETR:42;
A24: M9 is being_line by A3, ANALMETR:43;
A25: N9 is being_line by A4, ANALMETR:43;
A26: ( a1 <> b1 implies ( a2 <> b2 & a3 <> b3 & a4 <> b4 ) )
proof
assume A27: a1 <> b1 ; ::_thesis: ( a2 <> b2 & a3 <> b3 & a4 <> b4 )
A28: now__::_thesis:_not_a4_=_b4
assume a4 = b4 ; ::_thesis: contradiction
then a4,a1 // a4,b1 by A23, ANALMETR:59;
then LIN a4,a1,b1 by ANALMETR:def_10;
then LIN a49,a19,b19 by ANALMETR:40;
then LIN a19,b19,a49 by AFF_1:6;
hence contradiction by A5, A7, A13, A24, A27, AFF_1:25; ::_thesis: verum
end;
A29: now__::_thesis:_not_a2_=_b2
assume a2 = b2 ; ::_thesis: contradiction
then LIN a2,a1,b1 by A22, ANALMETR:def_10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5, A7, A14, A24, A27, AFF_1:25; ::_thesis: verum
end;
A30: now__::_thesis:_not_a3_=_b3
assume a3 = b3 ; ::_thesis: contradiction
then LIN a3,a2,b2 by A21, ANALMETR:def_10;
then LIN a39,a29,b29 by ANALMETR:40;
then LIN a29,b29,a39 by AFF_1:6;
hence contradiction by A9, A11, A18, A25, A29, AFF_1:25; ::_thesis: verum
end;
assume ( a2 = b2 or a3 = b3 or a4 = b4 ) ; ::_thesis: contradiction
hence contradiction by A29, A28, A30; ::_thesis: verum
end;
A31: now__::_thesis:_(_a1_<>_b1_implies_a3,a4_//_b3,b4_)
assume A32: a1 <> b1 ; ::_thesis: a3,a4 // b3,b4
A33: now__::_thesis:_(_a2_=_a4_implies_a3,a4_//_b3,b4_)
A34: not LIN a29,b19,b29
proof
assume LIN a29,b19,b29 ; ::_thesis: contradiction
then LIN a29,b29,b19 by AFF_1:6;
hence contradiction by A9, A11, A19, A25, A26, A32, AFF_1:25; ::_thesis: verum
end;
assume A35: a2 = a4 ; ::_thesis: a3,a4 // b3,b4
then a2,a1 // b1,b4 by A23, ANALMETR:59;
then b2,b1 // b1,b4 by A5, A14, A22, ANALMETR:60;
then b1,b2 // b1,b4 by ANALMETR:59;
then A36: b19,b29 // b19,b49 by ANALMETR:36;
a29,b29 // a29,b49 by A9, A11, A12, A25, AFF_1:39, AFF_1:41;
then LIN a29,b29,b49 by AFF_1:def_1;
hence a3,a4 // b3,b4 by A21, A35, A34, A36, AFF_1:14; ::_thesis: verum
end;
A37: now__::_thesis:_(_a2_<>_a4_&_a1_<>_a3_implies_a3,a4_//_b3,b4_)
assume that
A38: a2 <> a4 and
A39: a1 <> a3 ; ::_thesis: a3,a4 // b3,b4
A40: now__::_thesis:_(_M_//_N_implies_a3,a4_//_b3,b4_)
consider e1 being Element of X such that
A41: b1,b2 // b1,e1 and
A42: b1 <> e1 by ANALMETR:39;
consider x being Element of X such that
A43: LIN a1,a2,x and
A44: a1 <> x and
A45: a2 <> x by Th2;
reconsider x9 = x as Element of (Af X) by ANALMETR:35;
consider e2 being Element of X such that
A46: a1,b1 // x,e2 and
A47: x <> e2 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
not b19,e19 // x9,e29
proof
assume b19,e19 // x9,e29 ; ::_thesis: contradiction
then b1,e1 // x,e2 by ANALMETR:36;
then b1,b2 // x,e2 by A41, A42, ANALMETR:60;
then b1,b2 // a1,b1 by A46, A47, ANALMETR:60;
then b1,a1 // b1,b2 by ANALMETR:59;
then LIN b1,a1,b2 by ANALMETR:def_10;
then LIN b19,a19,b29 by ANALMETR:40;
hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; ::_thesis: verum
end;
then consider y9 being Element of (Af X) such that
A48: LIN b19,e19,y9 and
A49: LIN x9,e29,y9 by AFF_1:60;
reconsider y = y9 as Element of X by ANALMETR:35;
A50: a1,a2 // a1,x by A43, ANALMETR:def_10;
A51: not LIN a2,b2,x
proof
A52: a2 <> b2
proof
assume a2 = b2 ; ::_thesis: contradiction
then LIN a2,a1,b1 by A22, ANALMETR:def_10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; ::_thesis: verum
end;
LIN a19,a29,x9 by A43, ANALMETR:40;
then A53: LIN a29,x9,a19 by AFF_1:6;
assume LIN a2,b2,x ; ::_thesis: contradiction
then LIN a29,b29,x9 by ANALMETR:40;
then x9 in N9 by A9, A11, A25, A52, AFF_1:25;
hence contradiction by A9, A17, A25, A45, A53, AFF_1:25; ::_thesis: verum
end;
A54: not LIN a1,b1,a4
proof
assume LIN a1,b1,a4 ; ::_thesis: contradiction
then LIN a19,b19,a49 by ANALMETR:40;
hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; ::_thesis: verum
end;
A55: not LIN a1,b1,x
proof
assume LIN a1,b1,x ; ::_thesis: contradiction
then LIN a19,b19,x9 by ANALMETR:40;
then A56: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A56, AFF_1:25; ::_thesis: verum
end;
assume A57: M // N ; ::_thesis: a3,a4 // b3,b4
then M9 // N9 by ANALMETR:46;
then a39,b39 // a29,b29 by A6, A8, A9, A11, AFF_1:39;
then a3,b3 // a2,b2 by ANALMETR:36;
then A58: a2,b2 // a3,b3 by ANALMETR:59;
LIN x,e2,y by A49, ANALMETR:40;
then x,e2 // x,y by ANALMETR:def_10;
then A59: a1,b1 // x,y by A46, A47, ANALMETR:60;
A60: b1 <> y
proof
assume b1 = y ; ::_thesis: contradiction
then b1,a1 // b1,x by A59, ANALMETR:59;
then LIN b1,a1,x by ANALMETR:def_10;
then LIN b19,a19,x9 by ANALMETR:40;
then A61: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A61, AFF_1:25; ::_thesis: verum
end;
LIN b1,e1,y by A48, ANALMETR:40;
then b1,e1 // b1,y by ANALMETR:def_10;
then A62: b1,b2 // b1,y by A41, A42, ANALMETR:60;
then LIN b1,b2,y by ANALMETR:def_10;
then LIN b19,b29,y9 by ANALMETR:40;
then LIN y9,b19,b29 by AFF_1:6;
then LIN y,b1,b2 by ANALMETR:40;
then y,b1 // y,b2 by ANALMETR:def_10;
then A63: b1,y // b2,y by ANALMETR:59;
a1,a2 // b1,b2 by A22, ANALMETR:59;
then a1,a2 // b1,y by A7, A15, A62, ANALMETR:60;
then A64: a1,x // b1,y by A5, A14, A50, ANALMETR:60;
A65: not LIN x,y,a3
proof
A66: x <> y
proof
assume x = y ; ::_thesis: contradiction
then x,a1 // x,b1 by A64, ANALMETR:59;
then LIN x,a1,b1 by ANALMETR:def_10;
then LIN x9,a19,b19 by ANALMETR:40;
then LIN a19,b19,x9 by AFF_1:6;
then A67: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN x9,a19,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A67, AFF_1:25; ::_thesis: verum
end;
a19,a39 // a19,b19 by A5, A6, A7, A24, AFF_1:39, AFF_1:41;
then a1,a3 // a1,b1 by ANALMETR:36;
then A68: x,y // a1,a3 by A32, A59, ANALMETR:60;
assume LIN x,y,a3 ; ::_thesis: contradiction
then x,y // x,a3 by ANALMETR:def_10;
then x,a3 // a1,a3 by A66, A68, ANALMETR:60;
then a3,a1 // a3,x by ANALMETR:59;
then LIN a3,a1,x by ANALMETR:def_10;
then LIN a39,a19,x9 by ANALMETR:40;
then A69: x9 in M9 by A5, A6, A24, A39, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a19,x9,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A69, AFF_1:25; ::_thesis: verum
end;
A70: not LIN x,y,a4
proof
A71: x <> y
proof
assume x = y ; ::_thesis: contradiction
then x,a1 // x,b1 by A64, ANALMETR:59;
then LIN x,a1,b1 by ANALMETR:def_10;
then LIN x9,a19,b19 by ANALMETR:40;
then LIN a19,b19,x9 by AFF_1:6;
then A72: x9 in M9 by A5, A7, A24, A32, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN x9,a19,a29 by AFF_1:6;
hence contradiction by A5, A14, A24, A44, A72, AFF_1:25; ::_thesis: verum
end;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a29,a49 by A5, A7, A9, A10, AFF_1:39;
then a1,b1 // a2,a4 by ANALMETR:36;
then A73: a2,a4 // x,y by A32, A59, ANALMETR:60;
assume LIN x,y,a4 ; ::_thesis: contradiction
then x,y // x,a4 by ANALMETR:def_10;
then a2,a4 // x,a4 by A71, A73, ANALMETR:60;
then a4,a2 // a4,x by ANALMETR:59;
then LIN a4,a2,x by ANALMETR:def_10;
then LIN a49,a29,x9 by ANALMETR:40;
then A74: x9 in N9 by A9, A10, A25, A38, AFF_1:25;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN a29,x9,a19 by AFF_1:6;
hence contradiction by A9, A17, A25, A45, A74, AFF_1:25; ::_thesis: verum
end;
A75: not LIN a2,b2,a3
proof
A76: a2 <> b2
proof
assume a2 = b2 ; ::_thesis: contradiction
then LIN a2,a1,b1 by A22, ANALMETR:def_10;
then LIN a29,a19,b19 by ANALMETR:40;
then LIN a19,b19,a29 by AFF_1:6;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; ::_thesis: verum
end;
assume LIN a2,b2,a3 ; ::_thesis: contradiction
then LIN a29,b29,a39 by ANALMETR:40;
hence contradiction by A9, A11, A18, A25, A76, AFF_1:25; ::_thesis: verum
end;
A77: ( X is satisfying_TDES implies X is satisfying_des )
proof
assume X is satisfying_TDES ; ::_thesis: X is satisfying_des
then Af X is Moufangian by Th7;
then Af X is translational by AFF_2:14;
hence X is satisfying_des by Th8; ::_thesis: verum
end;
LIN a19,a29,x9 by A43, ANALMETR:40;
then LIN x9,a19,a29 by AFF_1:6;
then LIN x,a1,a2 by ANALMETR:40;
then x,a1 // x,a2 by ANALMETR:def_10;
then a1,x // a2,x by ANALMETR:59;
then a2,x // b1,y by A44, A64, ANALMETR:60;
then A78: a2,x // b2,y by A60, A63, ANALMETR:60;
a19,b19 // a39,b39 by A5, A6, A7, A8, A24, AFF_1:39, AFF_1:41;
then a1,b1 // a3,b3 by ANALMETR:36;
then A79: x,y // a3,b3 by A32, A59, ANALMETR:60;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;
then a1,b1 // a4,b4 by ANALMETR:36;
then A80: x,y // a4,b4 by A32, A59, ANALMETR:60;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a29,b29 by A5, A7, A9, A11, AFF_1:39;
then a1,b1 // a2,b2 by ANALMETR:36;
then A81: a2,b2 // x,y by A32, A59, ANALMETR:60;
a2,a3 // b2,b3 by A21, ANALMETR:59;
then A82: x,a3 // y,b3 by A2, A77, A51, A75, A81, A58, A78, Def8;
M9 // N9 by A57, ANALMETR:46;
then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;
then a1,b1 // a4,b4 by ANALMETR:36;
then x,a4 // y,b4 by A2, A23, A59, A77, A55, A54, A64, Def8;
hence a3,a4 // b3,b4 by A2, A77, A82, A65, A70, A79, A80, Def8; ::_thesis: verum
end;
now__::_thesis:_(_not_M_//_N_implies_a3,a4_//_b3,b4_)
assume not M // N ; ::_thesis: a3,a4 // b3,b4
then not M9 // N9 by ANALMETR:46;
then consider o9 being Element of (Af X) such that
A83: o9 in M9 and
A84: o9 in N9 by A24, A25, AFF_1:58;
reconsider o = o9 as Element of X by ANALMETR:35;
consider K being Subset of X such that
A85: o in K and
A86: N _|_ K by A4, Th3;
reconsider K9 = K as Subset of (Af X) by ANALMETR:42;
A87: K is being_line by A86, ANALMETR:44;
then A88: K9 is being_line by ANALMETR:43;
now__::_thesis:_(_K_<>_M_implies_a3,a4_//_b3,b4_)
A89: ( not a2 in K & not a4 in K & not b2 in K & not b4 in K )
proof
A90: now__::_thesis:_for_x_being_Element_of_X_st_x_in_N_&_o_<>_x_holds_
not_x_in_K
let x be Element of X; ::_thesis: ( x in N & o <> x implies not x in K )
assume that
A91: x in N and
A92: o <> x ; ::_thesis: not x in K
assume x in K ; ::_thesis: contradiction
then o,x _|_ o,x by A84, A85, A86, A91, ANALMETR:56;
hence contradiction by A92, ANALMETR:39; ::_thesis: verum
end;
assume ( a2 in K or a4 in K or b2 in K or b4 in K ) ; ::_thesis: contradiction
hence contradiction by A9, A10, A11, A12, A13, A14, A15, A16, A83, A90; ::_thesis: verum
end;
A93: LIN o,a2,b2 by A4, A9, A11, A84, Th4;
A94: now__::_thesis:_not_LIN_a1,b1,a4
assume LIN a1,b1,a4 ; ::_thesis: contradiction
then LIN a19,b19,a49 by ANALMETR:40;
hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; ::_thesis: verum
end;
A95: LIN o,a3,b3 by A3, A6, A8, A83, Th4;
A96: now__::_thesis:_not_LIN_a3,b3,a2
assume LIN a3,b3,a2 ; ::_thesis: contradiction
then LIN a39,b39,a29 by ANALMETR:40;
hence contradiction by A6, A8, A14, A24, A26, A32, AFF_1:25; ::_thesis: verum
end;
A97: LIN o,a1,b1 by A3, A5, A7, A83, Th4;
A98: now__::_thesis:_for_x9_being_Element_of_(Af_X)_ex_y9_being_Element_of_(Af_X)_st_
(_y9_in_K9_&_x9,y9_//_N9_)
let x9 be Element of (Af X); ::_thesis: ex y9 being Element of (Af X) st
( y9 in K9 & x9,y9 // N9 )
consider D9 being Subset of (Af X) such that
A99: x9 in D9 and
A100: N9 // D9 by A25, AFF_1:49;
reconsider D = D9 as Subset of the carrier of X by ANALMETR:42;
N // D by A100, ANALMETR:46;
then K _|_ D by A86, ANALMETR:52;
then consider y being Element of X such that
A101: y in K and
A102: y in D by ANALMETR:66;
reconsider y9 = y as Element of (Af X) by ANALMETR:35;
take y9 = y9; ::_thesis: ( y9 in K9 & x9,y9 // N9 )
thus ( y9 in K9 & x9,y9 // N9 ) by A99, A100, A101, A102, AFF_1:40; ::_thesis: verum
end;
then consider d19 being Element of (Af X) such that
A103: d19 in K9 and
A104: a19,d19 // N9 ;
consider e19 being Element of (Af X) such that
A105: e19 in K9 and
A106: b19,e19 // N9 by A98;
consider d39 being Element of (Af X) such that
A107: d39 in K9 and
A108: a39,d39 // N9 by A98;
consider e39 being Element of (Af X) such that
A109: e39 in K9 and
A110: b39,e39 // N9 by A98;
reconsider d1 = d19, d3 = d39, e1 = e19, e3 = e39 as Element of X by ANALMETR:35;
A111: LIN o,d1,e1 by A85, A87, A103, A105, Th4;
A112: ( o <> e1 & o <> e3 & o <> d1 & o <> d3 )
proof
A113: now__::_thesis:_for_x,_y_being_Element_of_X
for_x9,_y9_being_Element_of_(Af_X)_st_x9,y9_//_N9_&_x_=_x9_&_y_=_y9_&_x_in_M_&_y_in_K_&_not_x_in_N_holds_
not_o_=_y
let x, y be Element of X; ::_thesis: for x9, y9 being Element of (Af X) st x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N holds
not o = y
let x9, y9 be Element of (Af X); ::_thesis: ( x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N implies not o = y )
assume that
A114: x9,y9 // N9 and
A115: x = x9 and
A116: y = y9 and
x in M and
y in K and
A117: not x in N ; ::_thesis: not o = y
assume o = y ; ::_thesis: contradiction
then o9,x9 // N9 by A114, A116, AFF_1:34;
hence contradiction by A25, A84, A115, A117, AFF_1:23; ::_thesis: verum
end;
assume ( not o <> e1 or not o <> e3 or not o <> d1 or not o <> d3 ) ; ::_thesis: contradiction
hence contradiction by A5, A6, A7, A8, A17, A18, A19, A20, A103, A104, A107, A108, A109, A110, A105, A106, A113; ::_thesis: verum
end;
a1,d1 // o,a2 by A9, A84, A104, Th6;
then A118: d1,a1 // o,a2 by ANALMETR:59;
A119: not e1 in N by A19, A106, AFF_1:35;
A120: not d3 in N by A18, A108, AFF_1:35;
a19,d19 // b19,e19 by A25, A104, A106, AFF_1:31;
then a1,d1 // b1,e1 by ANALMETR:36;
then A121: d1,a1 // e1,b1 by ANALMETR:59;
assume A122: K <> M ; ::_thesis: a3,a4 // b3,b4
A123: now__::_thesis:_not_LIN_a3,b3,d3
assume LIN a3,b3,d3 ; ::_thesis: contradiction
then LIN a39,b39,d39 by ANALMETR:40;
then d3 in M by A6, A8, A24, A26, A32, AFF_1:25;
hence contradiction by A3, A83, A85, A87, A122, A107, A112, Th5; ::_thesis: verum
end;
A124: now__::_thesis:_not_LIN_a1,b1,d1
assume LIN a1,b1,d1 ; ::_thesis: contradiction
then LIN a19,b19,d19 by ANALMETR:40;
then d1 in M by A5, A7, A24, A32, AFF_1:25;
hence contradiction by A3, A83, A85, A87, A122, A103, A112, Th5; ::_thesis: verum
end;
a39,d39 // b39,e39 by A25, A108, A110, AFF_1:31;
then A125: a3,d3 // b3,e3 by ANALMETR:36;
then A126: d3,a3 // e3,b3 by ANALMETR:59;
A127: ( not LIN d3,e3,a3 & not LIN d3,e3,a4 )
proof
A128: d3 <> e3
proof
assume not d3 <> e3 ; ::_thesis: contradiction
then LIN e3,a3,b3 by A126, ANALMETR:def_10;
then LIN e39,a39,b39 by ANALMETR:40;
then LIN a39,b39,e39 by AFF_1:6;
then e39 in M9 by A6, A8, A24, A26, A32, AFF_1:25;
hence contradiction by A24, A83, A85, A88, A122, A109, A112, AFF_1:18; ::_thesis: verum
end;
assume ( LIN d3,e3,a3 or LIN d3,e3,a4 ) ; ::_thesis: contradiction
then ( LIN d39,e39,a39 or LIN d39,e39,a49 ) by ANALMETR:40;
then ( a39 in K9 or a49 in K9 ) by A88, A107, A109, A128, AFF_1:25;
hence contradiction by A6, A10, A13, A18, A24, A25, A83, A84, A85, A86, A88, A122, AFF_1:18; ::_thesis: verum
end;
A129: now__::_thesis:_not_LIN_a1,b1,a2
assume LIN a1,b1,a2 ; ::_thesis: contradiction
then LIN a19,b19,a29 by ANALMETR:40;
hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; ::_thesis: verum
end;
A130: LIN o,a4,b4 by A4, A10, A12, A84, Th4;
a1,a2 // b1,b2 by A22, ANALMETR:59;
then d1,a2 // e1,b2 by A2, A14, A15, A17, A19, A83, A84, A112, A93, A97, A111, A124, A129, A121, A118, Def5;
then A131: a2,d1 // b2,e1 by ANALMETR:59;
A132: not e3 in N by A20, A110, AFF_1:35;
A133: LIN o,d3,e3 by A85, A87, A107, A109, Th4;
a1,d1 // o,a4 by A10, A84, A104, Th6;
then d1,a1 // o,a4 by ANALMETR:59;
then A134: d1,a4 // e1,b4 by A2, A13, A16, A17, A19, A23, A83, A84, A112, A97, A130, A111, A124, A94, A121, Def5;
A135: a3,d3 // o,a4 by A10, A84, A108, Th6;
A136: not d1 in N by A17, A104, AFF_1:35;
a3,d3 // o,a2 by A9, A84, A108, Th6;
then d3,a3 // o,a2 by ANALMETR:59;
then d3,a2 // e3,b2 by A2, A14, A15, A18, A20, A21, A83, A84, A112, A93, A95, A133, A123, A96, A126, Def5;
then d3,a4 // e3,b4 by A1, A9, A10, A11, A12, A86, A103, A107, A109, A105, A131, A134, A136, A120, A119, A132, A89, Def7;
hence a3,a4 // b3,b4 by A2, A13, A16, A18, A20, A83, A84, A112, A130, A95, A133, A125, A127, A135, Def5; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A86, Def7; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A40; ::_thesis: verum
end;
now__::_thesis:_(_a1_=_a3_implies_a3,a4_//_b3,b4_)
A137: not LIN a19,b29,b19
proof
assume LIN a19,b29,b19 ; ::_thesis: contradiction
then LIN a19,b19,b29 by AFF_1:6;
hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; ::_thesis: verum
end;
a19,b19 // a19,b39 by A5, A7, A8, A24, AFF_1:39, AFF_1:41;
then A138: LIN a19,b19,b39 by AFF_1:def_1;
assume A139: a1 = a3 ; ::_thesis: a3,a4 // b3,b4
then a2,a1 // b2,b3 by A21, ANALMETR:59;
then b2,b1 // b2,b3 by A5, A14, A22, ANALMETR:60;
then b29,b19 // b29,b39 by ANALMETR:36;
hence a3,a4 // b3,b4 by A23, A139, A137, A138, AFF_1:14; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A33, A37; ::_thesis: verum
end;
A140: ( a1 = b1 implies ( a2 = b2 & a3 = b3 & a4 = b4 ) )
proof
assume A141: a1 = b1 ; ::_thesis: ( a2 = b2 & a3 = b3 & a4 = b4 )
A142: now__::_thesis:_not_a4_<>_b4
LIN a1,a4,b4 by A23, A141, ANALMETR:def_10;
then LIN a19,a49,b49 by ANALMETR:40;
then A143: LIN a49,b49,a19 by AFF_1:6;
assume a4 <> b4 ; ::_thesis: contradiction
hence contradiction by A10, A12, A17, A25, A143, AFF_1:25; ::_thesis: verum
end;
A144: now__::_thesis:_not_a2_<>_b2
a1,a2 // a1,b2 by A22, A141, ANALMETR:59;
then LIN a1,a2,b2 by ANALMETR:def_10;
then LIN a19,a29,b29 by ANALMETR:40;
then A145: LIN a29,b29,a19 by AFF_1:6;
assume a2 <> b2 ; ::_thesis: contradiction
hence contradiction by A9, A11, A17, A25, A145, AFF_1:25; ::_thesis: verum
end;
A146: now__::_thesis:_not_a3_<>_b3
a2,a3 // a2,b3 by A21, A144, ANALMETR:59;
then LIN a2,a3,b3 by ANALMETR:def_10;
then LIN a29,a39,b39 by ANALMETR:40;
then A147: LIN a39,b39,a29 by AFF_1:6;
assume a3 <> b3 ; ::_thesis: contradiction
hence contradiction by A6, A8, A14, A24, A147, AFF_1:25; ::_thesis: verum
end;
assume ( a2 <> b2 or a3 <> b3 or a4 <> b4 ) ; ::_thesis: contradiction
hence contradiction by A144, A142, A146; ::_thesis: verum
end;
now__::_thesis:_(_a1_=_b1_implies_a3,a4_//_b3,b4_)
assume a1 = b1 ; ::_thesis: a3,a4 // b3,b4
then a39,a49 // b39,b49 by A140, AFF_1:2;
hence a3,a4 // b3,b4 by ANALMETR:36; ::_thesis: verum
end;
hence a3,a4 // b3,b4 by A31; ::_thesis: verum
end;
theorem :: CONMETR:13
for X being OrtAfPl st X is satisfying_OPAP & X is satisfying_DES holds
X is satisfying_PAP
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP )
assume that
A1: X is satisfying_OPAP and
A2: X is satisfying_DES ; ::_thesis: X is satisfying_PAP
let o be Element of X; :: according to CONMETR:def_2 ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let a1, a2, a3, b1, b2, b3 be Element of X; ::_thesis: for M, N being Subset of X st M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let M, N be Subset of X; ::_thesis: ( M is being_line & N is being_line & o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )
assume that
A3: M is being_line and
A4: N is being_line and
A5: o in M and
A6: a1 in M and
A7: a2 in M and
A8: a3 in M and
A9: o in N and
A10: b1 in N and
A11: b2 in N and
A12: b3 in N and
A13: not b2 in M and
A14: not a3 in N and
A15: o <> a1 and
A16: o <> a2 and
o <> a3 and
A17: o <> b1 and
o <> b2 and
A18: o <> b3 and
A19: a3,b2 // a2,b1 and
A20: a3,b3 // a1,b1 ; ::_thesis: a1,b2 // a2,b3
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of (Af X) by ANALMETR:35;
reconsider M9 = M, N9 = N as Subset of (Af X) by ANALMETR:42;
A21: M9 is being_line by A3, ANALMETR:43;
A22: N9 is being_line by A4, ANALMETR:43;
now__::_thesis:_(_not_M__|__N_implies_a1,b2_//_a2,b3_)
assume A23: not M _|_ N ; ::_thesis: a1,b2 // a2,b3
A24: now__::_thesis:_(_a1_<>_a2_&_a2_<>_a3_&_a1_<>_a3_implies_a1,b2_//_a2,b3_)
assume that
A25: a1 <> a2 and
A26: a2 <> a3 and
A27: a1 <> a3 ; ::_thesis: a1,b2 // a2,b3
A28: ( b1 <> b2 & b2 <> b3 & b1 <> b3 )
proof
A29: now__::_thesis:_not_b1_=_b3
A30: not LIN o9,b19,a19
proof
o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A31: LIN o9,a19,a39 by AFF_1:def_1;
assume LIN o9,b19,a19 ; ::_thesis: contradiction
then a19 in N9 by A9, A10, A17, A22, AFF_1:25;
hence contradiction by A9, A14, A15, A22, A31, AFF_1:25; ::_thesis: verum
end;
assume b1 = b3 ; ::_thesis: contradiction
then b1,a1 // b1,a3 by A20, ANALMETR:59;
then A32: b19,a19 // b19,a39 by ANALMETR:36;
o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a39 by AFF_1:def_1;
hence contradiction by A27, A30, A32, AFF_1:14; ::_thesis: verum
end;
A33: now__::_thesis:_not_b2_=_b3
A34: not LIN o9,b19,a19
proof
o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A35: LIN o9,a19,a39 by AFF_1:def_1;
assume LIN o9,b19,a19 ; ::_thesis: contradiction
then a19 in N9 by A9, A10, A17, A22, AFF_1:25;
hence contradiction by A9, A14, A15, A22, A35, AFF_1:25; ::_thesis: verum
end;
assume b2 = b3 ; ::_thesis: contradiction
then a1,b1 // a2,b1 by A8, A13, A19, A20, ANALMETR:60;
then b1,a1 // b1,a2 by ANALMETR:59;
then A36: b19,a19 // b19,a29 by ANALMETR:36;
o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a29 by AFF_1:def_1;
hence contradiction by A25, A34, A36, AFF_1:14; ::_thesis: verum
end;
A37: now__::_thesis:_not_b1_=_b2
A38: not LIN o9,b29,a29
proof
assume LIN o9,b29,a29 ; ::_thesis: contradiction
then LIN o9,a29,b29 by AFF_1:6;
hence contradiction by A5, A7, A13, A16, A21, AFF_1:25; ::_thesis: verum
end;
assume b1 = b2 ; ::_thesis: contradiction
then b2,a2 // b2,a3 by A19, ANALMETR:59;
then A39: b29,a29 // b29,a39 by ANALMETR:36;
o9,a29 // o9,a39 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a29,a39 by AFF_1:def_1;
hence contradiction by A26, A38, A39, AFF_1:14; ::_thesis: verum
end;
assume ( b1 = b2 or b2 = b3 or b1 = b3 ) ; ::_thesis: contradiction
hence contradiction by A37, A33, A29; ::_thesis: verum
end;
A40: now__::_thesis:_(_not_a3,b3__|__o,b2_implies_a1,b2_//_a2,b3_)
A41: not LIN b3,b1,a3
proof
assume LIN b3,b1,a3 ; ::_thesis: contradiction
then LIN b39,b19,a39 by ANALMETR:40;
hence contradiction by A10, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b39 by AFF_1:def_1;
then A42: LIN o,b2,b3 by ANALMETR:40;
A43: not LIN b2,b1,a3
proof
assume LIN b2,b1,a3 ; ::_thesis: contradiction
then LIN b29,b19,a39 by ANALMETR:40;
hence contradiction by A10, A11, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
o9,a39 // o9,a19 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a19 by AFF_1:def_1;
then A44: LIN o,a3,a1 by ANALMETR:40;
consider x being Element of X such that
A45: o,b2 _|_ o,x and
A46: o <> x by ANALMETR:39;
A47: o,x _|_ N by A4, A5, A9, A11, A13, A45, ANALMETR:55;
consider e19 being Element of (Af X) such that
A48: a39,b39 // b29,e19 and
A49: b29 <> e19 by DIRAF:40;
reconsider x9 = x as Element of (Af X) by ANALMETR:35;
LIN o9,x9,x9 by AFF_1:7;
then consider A9 being Subset of (Af X) such that
A50: A9 is being_line and
A51: o9 in A9 and
A52: x9 in A9 and
x9 in A9 by AFF_1:21;
reconsider A = A9 as Subset of X by ANALMETR:42;
A53: for e1 being Element of X st e1 in A holds
LIN o,x,e1
proof
let e1 be Element of X; ::_thesis: ( e1 in A implies LIN o,x,e1 )
assume A54: e1 in A ; ::_thesis: LIN o,x,e1
reconsider e19 = e1 as Element of (Af X) by ANALMETR:35;
o9,x9 // o9,e19 by A50, A51, A52, A54, AFF_1:39, AFF_1:41;
then LIN o9,x9,e19 by AFF_1:def_1;
hence LIN o,x,e1 by ANALMETR:40; ::_thesis: verum
end;
for e1 being Element of X st LIN o,x,e1 holds
e1 in A
proof
let e1 be Element of X; ::_thesis: ( LIN o,x,e1 implies e1 in A )
assume A55: LIN o,x,e1 ; ::_thesis: e1 in A
reconsider e19 = e1 as Element of (Af X) by ANALMETR:35;
LIN o9,x9,e19 by A55, ANALMETR:40;
hence e1 in A by A46, A50, A51, A52, AFF_1:25; ::_thesis: verum
end;
then A = Line (o,x) by A53, ANALMETR:def_11;
then A56: A _|_ N by A46, A47, ANALMETR:def_14;
A57: not b2 in A
proof
A58: o9,b29 // o9,b29 by AFF_1:2;
assume b2 in A ; ::_thesis: contradiction
then A9 // N9 by A5, A9, A11, A13, A22, A50, A51, A58, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A56, ANALMETR:52; ::_thesis: verum
end;
assume A59: not a3,b3 _|_ o,b2 ; ::_thesis: a1,b2 // a2,b3
not b29,e19 // A9
proof
assume A60: b29,e19 // A9 ; ::_thesis: contradiction
consider d19, d29 being Element of (Af X) such that
A61: d19 <> d29 and
A62: A9 = Line (d19,d29) by A50, AFF_1:def_3;
A63: d29 in A9 by A62, AFF_1:15;
reconsider d1 = d19, d2 = d29 as Element of X by ANALMETR:35;
d19,d29 // d19,d29 by AFF_1:2;
then d19,d29 // A9 by A61, A62, AFF_1:def_4;
then b29,e19 // d19,d29 by A50, A60, AFF_1:31;
then a39,b39 // d19,d29 by A48, A49, AFF_1:5;
then A64: a3,b3 // d1,d2 by ANALMETR:36;
d19 in A9 by A62, AFF_1:15;
then d1,d2 _|_ o,b2 by A9, A11, A56, A63, ANALMETR:56;
hence contradiction by A59, A61, A64, ANALMETR:62; ::_thesis: verum
end;
then consider c39 being Element of (Af X) such that
A65: c39 in A9 and
A66: LIN b29,e19,c39 by A50, AFF_1:59;
b29,e19 // b29,c39 by A66, AFF_1:def_1;
then A67: a39,b39 // b29,c39 by A48, A49, AFF_1:5;
consider e19 being Element of (Af X) such that
A68: c39,a39 // a19,e19 and
A69: a19 <> e19 by DIRAF:40;
not a19,e19 // A9
proof
A70: c39 <> o9
proof
assume c39 = o9 ; ::_thesis: contradiction
then A71: a3,b3 // b2,o by A67, ANALMETR:36;
b29,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then b2,o // b2,b3 by ANALMETR:36;
then a3,b3 // b2,b3 by A5, A13, A71, ANALMETR:60;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def_10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
assume A72: a19,e19 // A9 ; ::_thesis: contradiction
A73: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A50, A51, A65, AFF_1:40, AFF_1:41;
then a19,e19 // o9,c39 by A50, A72, AFF_1:31;
then c39,a39 // o9,c39 by A68, A69, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def_1;
then a39 in A9 by A50, A51, A65, A70, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A73, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
then consider c19 being Element of (Af X) such that
A74: c19 in A9 and
A75: LIN a19,e19,c19 by A50, AFF_1:59;
reconsider c1 = c19 as Element of X by ANALMETR:35;
reconsider c3 = c39 as Element of X by ANALMETR:35;
a19,e19 // a19,c19 by A75, AFF_1:def_1;
then A76: c39,a39 // a19,c19 by A68, A69, AFF_1:5;
then A77: c3,a3 // a1,c1 by ANALMETR:36;
consider e19 being Element of (Af X) such that
A78: c39,a39 // a29,e19 and
A79: a29 <> e19 by DIRAF:40;
not a29,e19 // A9
proof
A80: c39 <> o9
proof
assume c39 = o9 ; ::_thesis: contradiction
then A81: a3,b3 // b2,o by A67, ANALMETR:36;
b29,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then b2,o // b2,b3 by ANALMETR:36;
then a3,b3 // b2,b3 by A5, A13, A81, ANALMETR:60;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def_10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
assume A82: a29,e19 // A9 ; ::_thesis: contradiction
A83: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A50, A51, A65, AFF_1:40, AFF_1:41;
then a29,e19 // o9,c39 by A50, A82, AFF_1:31;
then c39,a39 // o9,c39 by A78, A79, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def_1;
then a39 in A9 by A50, A51, A65, A80, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A83, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
then consider c29 being Element of (Af X) such that
A84: c29 in A9 and
A85: LIN a29,e19,c29 by A50, AFF_1:59;
reconsider c2 = c29 as Element of X by ANALMETR:35;
a29,e19 // a29,c29 by A85, AFF_1:def_1;
then A86: c39,a39 // a29,c29 by A78, A79, AFF_1:5;
then A87: c3,a3 // a2,c2 by ANALMETR:36;
A88: ( o <> c3 & o <> c2 & o <> c1 )
proof
A89: now__::_thesis:_not_o_=_c3
assume A90: o = c3 ; ::_thesis: contradiction
b29,o9 // b39,b29 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then a39,b39 // b39,b29 by A5, A13, A67, A90, AFF_1:5;
then b39,b29 // b39,a39 by AFF_1:4;
then LIN b39,b29,a39 by AFF_1:def_1;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
A91: now__::_thesis:_(_not_o_=_c2_&_not_o_=_c1_)
a19,o9 // a19,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A92: a1,o // a1,a3 by ANALMETR:36;
assume ( o = c2 or o = c1 ) ; ::_thesis: contradiction
then A93: ( c3,a3 // a1,o or c3,a3 // a2,o ) by A76, A86, ANALMETR:36;
a29,o9 // a19,a39 by A5, A6, A7, A8, A21, AFF_1:39, AFF_1:41;
then a2,o // a1,a3 by ANALMETR:36;
then c3,a3 // a1,a3 by A15, A16, A93, A92, ANALMETR:60;
then a3,a1 // a3,c3 by ANALMETR:59;
then LIN a3,a1,c3 by ANALMETR:def_10;
then LIN a39,a19,c39 by ANALMETR:40;
then A94: c39 in M9 by A6, A8, A21, A27, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A65, A89, A94, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
assume ( o = c3 or o = c2 or o = c1 ) ; ::_thesis: contradiction
hence contradiction by A89, A91; ::_thesis: verum
end;
A95: not c3 in N
proof
A96: o9,c39 // o9,c39 by AFF_1:2;
assume c3 in N ; ::_thesis: contradiction
then A9 // N9 by A9, A22, A50, A51, A65, A88, A96, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A56, ANALMETR:52; ::_thesis: verum
end;
A97: not LIN a3,a2,c3
proof
assume LIN a3,a2,c3 ; ::_thesis: contradiction
then LIN a39,a29,c39 by ANALMETR:40;
then A98: c39 in M9 by A7, A8, A21, A26, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A65, A88, A98, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
A99: not LIN a3,a1,c3
proof
assume LIN a3,a1,c3 ; ::_thesis: contradiction
then LIN a39,a19,c39 by ANALMETR:40;
then A100: c39 in M9 by A6, A8, A21, A27, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A65, A88, A100, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
A101: not LIN a1,a2,c1
proof
assume LIN a1,a2,c1 ; ::_thesis: contradiction
then LIN a19,a29,c19 by ANALMETR:40;
then A102: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then M9 // A9 by A5, A21, A50, A51, A74, A88, A102, AFF_1:38;
then M // A by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a29 by AFF_1:def_1;
then A103: LIN o,a1,a2 by ANALMETR:40;
o9,b29 // o9,b19 by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b19 by AFF_1:def_1;
then A104: LIN o,b2,b1 by ANALMETR:40;
o9,c19 // o9,c29 by A50, A51, A74, A84, AFF_1:39, AFF_1:41;
then LIN o9,c19,c29 by AFF_1:def_1;
then A105: LIN o,c1,c2 by ANALMETR:40;
o9,c39 // o9,c29 by A50, A51, A65, A84, AFF_1:39, AFF_1:41;
then LIN o9,c39,c29 by AFF_1:def_1;
then A106: LIN o,c3,c2 by ANALMETR:40;
o9,c39 // o9,c19 by A50, A51, A65, A74, AFF_1:39, AFF_1:41;
then LIN o9,c39,c19 by AFF_1:def_1;
then A107: LIN o,c3,c1 by ANALMETR:40;
c3 <> a3
proof
A108: o9,a39 // o9,a39 by AFF_1:2;
assume c3 = a3 ; ::_thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A65, A108, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
then a1,c1 // a2,c2 by A77, A87, ANALMETR:60;
then A109: c1,a1 // c2,a2 by ANALMETR:59;
A110: not LIN c1,c2,b2
proof
A111: c19 <> c29
proof
A112: c3 <> a3
proof
A113: o9,c39 // o9,c39 by AFF_1:2;
assume c3 = a3 ; ::_thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A65, A113, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
assume c19 = c29 ; ::_thesis: contradiction
then a1,c1 // a2,c1 by A77, A87, A112, ANALMETR:60;
then c1,a2 // c1,a1 by ANALMETR:59;
then LIN c1,a2,a1 by ANALMETR:def_10;
then LIN c19,a29,a19 by ANALMETR:40;
then LIN a19,a29,c19 by AFF_1:6;
then A114: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A74, A88, A114, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; ::_thesis: verum
end;
assume LIN c1,c2,b2 ; ::_thesis: contradiction
then LIN c19,c29,b29 by ANALMETR:40;
then b29 in A9 by A50, A74, A84, A111, AFF_1:25;
then A9 = N9 by A5, A9, A11, A13, A22, A50, A51, AFF_1:18;
then A9 // N9 by A22, AFF_1:41;
then A // N by ANALMETR:46;
hence contradiction by A56, ANALMETR:52; ::_thesis: verum
end;
o9,a39 // o9,a29 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a29 by AFF_1:def_1;
then A115: LIN o,a3,a2 by ANALMETR:40;
o9,b39 // o9,b19 by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b39,b19 by AFF_1:def_1;
then A116: LIN o,b3,b1 by ANALMETR:40;
a3,c3 // a1,c1 by A77, ANALMETR:59;
then b3,c3 // b1,c1 by A2, A9, A14, A15, A17, A18, A20, A88, A99, A41, A44, A116, A107, CONAFFM:def_1;
then A117: c3,b3 // c1,b1 by ANALMETR:59;
a3,c3 // a2,c2 by A87, ANALMETR:59;
then b2,c3 // b1,c2 by A2, A5, A9, A13, A14, A16, A17, A19, A88, A115, A104, A106, A43, A97, CONAFFM:def_1;
then c3,b2 // c2,b1 by ANALMETR:59;
then c1,b2 // c2,b3 by A1, A9, A10, A11, A12, A17, A18, A51, A56, A65, A74, A84, A88, A117, A57, A95, Def1;
hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A88, A103, A42, A105, A101, A110, A109, CONAFFM:def_1; ::_thesis: verum
end;
now__::_thesis:_(_a3,b3__|__o,b2_implies_a1,b2_//_a2,b3_)
o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a29 by AFF_1:def_1;
then A118: LIN o,a1,a2 by ANALMETR:40;
o9,b29 // o9,b19 by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b19 by AFF_1:def_1;
then A119: LIN o,b2,b1 by ANALMETR:40;
o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b39 by AFF_1:def_1;
then A120: LIN o,b2,b3 by ANALMETR:40;
A121: ( not LIN b3,b1,a3 & not LIN b2,b1,a3 )
proof
assume ( LIN b3,b1,a3 or LIN b2,b1,a3 ) ; ::_thesis: contradiction
then ( LIN b39,b19,a39 or LIN b29,b19,a39 ) by ANALMETR:40;
hence contradiction by A10, A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
o9,a39 // o9,a29 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a29 by AFF_1:def_1;
then A122: LIN o,a3,a2 by ANALMETR:40;
o9,b39 // o9,b19 by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b39,b19 by AFF_1:def_1;
then A123: LIN o,b3,b1 by ANALMETR:40;
o9,a39 // o9,a19 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a19 by AFF_1:def_1;
then A124: LIN o,a3,a1 by ANALMETR:40;
consider x being Element of X such that
A125: o,b2 _|_ o,x and
A126: o <> x by ANALMETR:39;
A127: o,x _|_ N by A4, A5, A9, A11, A13, A125, ANALMETR:55;
consider e19 being Element of (Af X) such that
A128: a39,b29 // b39,e19 and
A129: b39 <> e19 by DIRAF:40;
reconsider x9 = x as Element of (Af X) by ANALMETR:35;
LIN o9,x9,x9 by AFF_1:7;
then consider A9 being Subset of (Af X) such that
A130: A9 is being_line and
A131: o9 in A9 and
A132: x9 in A9 and
x9 in A9 by AFF_1:21;
reconsider A = A9 as Subset of X by ANALMETR:42;
A133: for e1 being Element of X st e1 in A holds
LIN o,x,e1
proof
let e1 be Element of X; ::_thesis: ( e1 in A implies LIN o,x,e1 )
assume A134: e1 in A ; ::_thesis: LIN o,x,e1
reconsider e19 = e1 as Element of (Af X) by ANALMETR:35;
o9,x9 // o9,e19 by A130, A131, A132, A134, AFF_1:39, AFF_1:41;
then LIN o9,x9,e19 by AFF_1:def_1;
hence LIN o,x,e1 by ANALMETR:40; ::_thesis: verum
end;
for e1 being Element of X st LIN o,x,e1 holds
e1 in A
proof
let e1 be Element of X; ::_thesis: ( LIN o,x,e1 implies e1 in A )
assume A135: LIN o,x,e1 ; ::_thesis: e1 in A
reconsider e19 = e1 as Element of (Af X) by ANALMETR:35;
LIN o9,x9,e19 by A135, ANALMETR:40;
hence e1 in A by A126, A130, A131, A132, AFF_1:25; ::_thesis: verum
end;
then A = Line (o,x) by A133, ANALMETR:def_11;
then A136: A _|_ N by A126, A127, ANALMETR:def_14;
assume A137: a3,b3 _|_ o,b2 ; ::_thesis: a1,b2 // a2,b3
not b39,e19 // A9
proof
assume A138: b39,e19 // A9 ; ::_thesis: contradiction
consider d19, d29 being Element of (Af X) such that
A139: d19 <> d29 and
A140: A9 = Line (d19,d29) by A130, AFF_1:def_3;
A141: d29 in A9 by A140, AFF_1:15;
reconsider d1 = d19, d2 = d29 as Element of X by ANALMETR:35;
d19,d29 // d19,d29 by AFF_1:2;
then d19,d29 // A9 by A139, A140, AFF_1:def_4;
then b39,e19 // d19,d29 by A130, A138, AFF_1:31;
then a39,b29 // d19,d29 by A128, A129, AFF_1:5;
then A142: a3,b2 // d1,d2 by ANALMETR:36;
d19 in A9 by A140, AFF_1:15;
then d1,d2 _|_ o,b2 by A9, A11, A136, A141, ANALMETR:56;
then a3,b2 _|_ o,b2 by A139, A142, ANALMETR:62;
then a3,b2 // a3,b3 by A5, A13, A137, ANALMETR:63;
then LIN a3,b2,b3 by ANALMETR:def_10;
then LIN a39,b29,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
then consider c39 being Element of (Af X) such that
A143: c39 in A9 and
A144: LIN b39,e19,c39 by A130, AFF_1:59;
A145: b39,e19 // b39,c39 by A144, AFF_1:def_1;
consider e19 being Element of (Af X) such that
A146: c39,a39 // a29,e19 and
A147: a29 <> e19 by DIRAF:40;
not a29,e19 // A9
proof
A148: c39 <> o9
proof
assume c39 = o9 ; ::_thesis: contradiction
then A149: a39,b29 // b39,o9 by A128, A129, A145, AFF_1:5;
b39,o9 // b39,b29 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then a39,b29 // b39,b29 by A18, A149, AFF_1:5;
then b29,b39 // b29,a39 by AFF_1:4;
then LIN b29,b39,a39 by AFF_1:def_1;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
assume A150: a29,e19 // A9 ; ::_thesis: contradiction
A151: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A130, A131, A143, AFF_1:40, AFF_1:41;
then a29,e19 // o9,c39 by A130, A150, AFF_1:31;
then c39,a39 // o9,c39 by A146, A147, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def_1;
then a39 in A9 by A130, A131, A143, A148, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A151, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
then consider c29 being Element of (Af X) such that
A152: c29 in A9 and
A153: LIN a29,e19,c29 by A130, AFF_1:59;
reconsider c3 = c39 as Element of X by ANALMETR:35;
reconsider c2 = c29 as Element of X by ANALMETR:35;
a29,e19 // a29,c29 by A153, AFF_1:def_1;
then c39,a39 // a29,c29 by A146, A147, AFF_1:5;
then A154: c3,a3 // a2,c2 by ANALMETR:36;
then A155: a3,c3 // a2,c2 by ANALMETR:59;
consider e19 being Element of (Af X) such that
A156: c39,a39 // a19,e19 and
A157: a19 <> e19 by DIRAF:40;
not a19,e19 // A9
proof
A158: c39 <> o9
proof
assume c39 = o9 ; ::_thesis: contradiction
then A159: a39,b29 // b39,o9 by A128, A129, A145, AFF_1:5;
b39,o9 // b39,b29 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then a39,b29 // b39,b29 by A18, A159, AFF_1:5;
then b29,b39 // b29,a39 by AFF_1:4;
then LIN b29,b39,a39 by AFF_1:def_1;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
assume A160: a19,e19 // A9 ; ::_thesis: contradiction
A161: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A130, A131, A143, AFF_1:40, AFF_1:41;
then a19,e19 // o9,c39 by A130, A160, AFF_1:31;
then c39,a39 // o9,c39 by A156, A157, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def_1;
then a39 in A9 by A130, A131, A143, A158, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A161, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
then consider c19 being Element of (Af X) such that
A162: c19 in A9 and
A163: LIN a19,e19,c19 by A130, AFF_1:59;
reconsider c1 = c19 as Element of X by ANALMETR:35;
a19,e19 // a19,c19 by A163, AFF_1:def_1;
then c39,a39 // a19,c19 by A156, A157, AFF_1:5;
then A164: c3,a3 // a1,c1 by ANALMETR:36;
then A165: a3,c3 // a1,c1 by ANALMETR:59;
A166: a39,b29 // b39,c39 by A128, A129, A145, AFF_1:5;
A167: ( o <> c3 & o <> c2 & o <> c1 )
proof
A168: now__::_thesis:_not_o_=_c3
assume o = c3 ; ::_thesis: contradiction
then A169: a3,b2 // b3,o by A166, ANALMETR:36;
b39,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then b3,o // b2,b3 by ANALMETR:36;
then a3,b2 // b2,b3 by A18, A169, ANALMETR:60;
then b2,b3 // b2,a3 by ANALMETR:59;
then LIN b2,b3,a3 by ANALMETR:def_10;
then LIN b29,b39,a39 by ANALMETR:40;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; ::_thesis: verum
end;
A170: now__::_thesis:_(_not_o_=_c2_&_not_o_=_c1_)
a29,o9 // a29,a39 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then A171: a2,o // a2,a3 by ANALMETR:36;
assume ( o = c2 or o = c1 ) ; ::_thesis: contradiction
then A172: ( a3,c3 // a2,o or a3,c3 // a1,o ) by A154, A164, ANALMETR:59;
a19,o9 // a29,a39 by A5, A6, A7, A8, A21, AFF_1:39, AFF_1:41;
then a1,o // a2,a3 by ANALMETR:36;
then a3,c3 // a2,a3 by A15, A16, A172, A171, ANALMETR:60;
then a3,a2 // a3,c3 by ANALMETR:59;
then LIN a3,a2,c3 by ANALMETR:def_10;
then LIN a39,a29,c39 by ANALMETR:40;
then A173: c39 in M9 by A7, A8, A21, A26, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A143, A168, A173, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
assume ( o = c3 or o = c2 or o = c1 ) ; ::_thesis: contradiction
hence contradiction by A168, A170; ::_thesis: verum
end;
A174: not c3 in N
proof
A175: o9,c39 // o9,c39 by AFF_1:2;
assume c3 in N ; ::_thesis: contradiction
then A9 // N9 by A9, A22, A130, A131, A143, A167, A175, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A136, ANALMETR:52; ::_thesis: verum
end;
A176: not LIN a1,a2,c1
proof
assume LIN a1,a2,c1 ; ::_thesis: contradiction
then LIN a19,a29,c19 by ANALMETR:40;
then A177: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A162, A167, A177, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
A178: ( not LIN a3,a1,c3 & not LIN a3,a2,c3 )
proof
assume ( LIN a3,a1,c3 or LIN a3,a2,c3 ) ; ::_thesis: contradiction
then ( LIN a39,a19,c39 or LIN a39,a29,c39 ) by ANALMETR:40;
then A179: ( c39 in M9 or c39 in M9 ) by A6, A7, A8, A21, A26, A27, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A143, A167, A179, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
A180: not b2 in A
proof
A181: o9,b29 // o9,b29 by AFF_1:2;
assume b2 in A ; ::_thesis: contradiction
then A9 // N9 by A5, A9, A11, A13, A22, A130, A131, A181, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A136, ANALMETR:52; ::_thesis: verum
end;
A182: not LIN c1,c2,b2
proof
A183: c19 <> c29
proof
A184: a3 <> c3
proof
A185: o9,c39 // o9,c39 by AFF_1:2;
assume a3 = c3 ; ::_thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A143, A185, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
assume c19 = c29 ; ::_thesis: contradiction
then a2,c1 // a1,c1 by A155, A165, A184, ANALMETR:60;
then c1,a1 // c1,a2 by ANALMETR:59;
then LIN c1,a1,a2 by ANALMETR:def_10;
then LIN c19,a19,a29 by ANALMETR:40;
then LIN a19,a29,c19 by AFF_1:6;
then A186: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A162, A167, A186, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
assume LIN c1,c2,b2 ; ::_thesis: contradiction
then LIN c19,c29,b29 by ANALMETR:40;
hence contradiction by A130, A152, A162, A180, A183, AFF_1:25; ::_thesis: verum
end;
o9,c19 // o9,c29 by A130, A131, A152, A162, AFF_1:39, AFF_1:41;
then LIN o9,c19,c29 by AFF_1:def_1;
then A187: LIN o,c1,c2 by ANALMETR:40;
a3 <> c3
proof
A188: o9,a39 // o9,a39 by AFF_1:2;
assume a3 = c3 ; ::_thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A143, A188, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; ::_thesis: verum
end;
then a2,c2 // a1,c1 by A155, A165, ANALMETR:60;
then A189: c1,a1 // c2,a2 by ANALMETR:59;
o9,c39 // o9,c19 by A130, A131, A143, A162, AFF_1:39, AFF_1:41;
then LIN o9,c39,c19 by AFF_1:def_1;
then LIN o,c3,c1 by ANALMETR:40;
then b3,c3 // b1,c1 by A2, A9, A14, A15, A17, A18, A20, A165, A167, A121, A178, A124, A123, CONAFFM:def_1;
then A190: c3,b3 // c1,b1 by ANALMETR:59;
o9,c39 // o9,c29 by A130, A131, A143, A152, AFF_1:39, AFF_1:41;
then LIN o9,c39,c29 by AFF_1:def_1;
then LIN o,c3,c2 by ANALMETR:40;
then b2,c3 // b1,c2 by A2, A5, A9, A13, A14, A16, A17, A19, A155, A167, A121, A178, A122, A119, CONAFFM:def_1;
then c3,b2 // c2,b1 by ANALMETR:59;
then c1,b2 // c2,b3 by A1, A9, A10, A11, A12, A17, A18, A131, A136, A143, A152, A162, A167, A190, A180, A174, Def1;
hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A167, A118, A120, A187, A176, A182, A189, CONAFFM:def_1; ::_thesis: verum
end;
hence a1,b2 // a2,b3 by A40; ::_thesis: verum
end;
A191: now__::_thesis:_(_a1_=_a3_implies_a1,b2_//_a2,b3_)
A192: not LIN o9,a39,b39
proof
assume LIN o9,a39,b39 ; ::_thesis: contradiction
then LIN o9,b39,a39 by AFF_1:6;
hence contradiction by A9, A12, A14, A18, A22, AFF_1:25; ::_thesis: verum
end;
o9,b39 // o9,b19 by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then A193: LIN o9,b39,b19 by AFF_1:def_1;
assume A194: a1 = a3 ; ::_thesis: a1,b2 // a2,b3
then a39,b39 // a39,b19 by A20, ANALMETR:36;
hence a1,b2 // a2,b3 by A19, A194, A192, A193, AFF_1:14; ::_thesis: verum
end;
A195: now__::_thesis:_(_a1_=_a2_implies_a1,b2_//_a2,b3_)
o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then A196: LIN o9,b29,b39 by AFF_1:def_1;
assume A197: a1 = a2 ; ::_thesis: a1,b2 // a2,b3
a1 <> b1
proof
o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A198: LIN o9,a19,a39 by AFF_1:def_1;
assume a1 = b1 ; ::_thesis: contradiction
hence contradiction by A9, A10, A14, A15, A22, A198, AFF_1:25; ::_thesis: verum
end;
then a3,b2 // a3,b3 by A19, A20, A197, ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29 = b39 by A5, A8, A9, A13, A14, A21, A196, AFF_1:14, AFF_1:25;
then a19,b29 // a29,b39 by A197, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum
end;
now__::_thesis:_(_a2_=_a3_implies_a1,b2_//_a2,b3_)
o9,b29 // o9,b19 by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then A199: LIN o9,b29,b19 by AFF_1:def_1;
assume A200: a2 = a3 ; ::_thesis: a1,b2 // a2,b3
then a39,b29 // a39,b19 by A19, ANALMETR:36;
then b29 = b19 by A5, A8, A9, A13, A14, A21, A199, AFF_1:14, AFF_1:25;
hence a1,b2 // a2,b3 by A20, A200, ANALMETR:59; ::_thesis: verum
end;
hence a1,b2 // a2,b3 by A195, A191, A24; ::_thesis: verum
end;
hence a1,b2 // a2,b3 by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Def1; ::_thesis: verum
end;
theorem :: CONMETR:14
for X being OrtAfPl st X is satisfying_MH1 & X is satisfying_MH2 holds
X is satisfying_OPAP
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP )
assume A1: X is satisfying_MH1 ; ::_thesis: ( not X is satisfying_MH2 or X is satisfying_OPAP )
assume A2: X is satisfying_MH2 ; ::_thesis: X is satisfying_OPAP
let o be Element of X; :: according to CONMETR:def_1 ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let a1, a2, a3, b1, b2, b3 be Element of X; ::_thesis: for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let M, N be Subset of X; ::_thesis: ( o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )
assume that
A3: o in M and
A4: a1 in M and
A5: a2 in M and
A6: a3 in M and
A7: o in N and
A8: b1 in N and
A9: b2 in N and
A10: b3 in N and
A11: not b2 in M and
A12: not a3 in N and
A13: M _|_ N and
A14: o <> a1 and
A15: o <> a2 and
o <> a3 and
A16: o <> b1 and
o <> b2 and
A17: o <> b3 and
A18: a3,b2 // a2,b1 and
A19: a3,b3 // a1,b1 ; ::_thesis: a1,b2 // a2,b3
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of (Af X) by ANALMETR:35;
reconsider M9 = M, N9 = N as Subset of (Af X) by ANALMETR:42;
N is being_line by A13, ANALMETR:44;
then A20: N9 is being_line by ANALMETR:43;
M is being_line by A13, ANALMETR:44;
then A21: M9 is being_line by ANALMETR:43;
A22: now__::_thesis:_(_a1_<>_a2_&_a2_<>_a3_&_a1_<>_a3_implies_ex_d4_being_Element_of_X_st_a1,b2_//_a2,b3_)
consider e1 being Element of X such that
A23: o,a3 // o,e1 and
A24: o <> e1 by ANALMETR:39;
consider d1 being Element of X such that
A25: o,b3 // o,d1 and
A26: o <> d1 by ANALMETR:39;
reconsider d19 = d1 as Element of (Af X) by ANALMETR:35;
consider e2 being Element of X such that
A27: a1,b3 _|_ d1,e2 and
A28: d1 <> e2 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
assume that
A29: a1 <> a2 and
a2 <> a3 and
A30: a1 <> a3 ; ::_thesis: ex d4 being Element of X st a1,b2 // a2,b3
A31: LIN o,b3,d1 by A25, ANALMETR:def_10;
then A32: LIN o9,b39,d19 by ANALMETR:40;
N is being_line by A13, ANALMETR:44;
then A33: N9 is being_line by ANALMETR:43;
then A34: o9,b29 // o9,b39 by A7, A9, A10, AFF_1:39, AFF_1:41;
then o,b2 // o,b3 by ANALMETR:36;
then A35: LIN o,b2,b3 by ANALMETR:def_10;
A36: b2 <> b3
proof
A37: not LIN o9,b19,a29
proof
o9,a29 // o9,a39 by A3, A5, A6, A21, AFF_1:39, AFF_1:41;
then A38: LIN o9,a29,a39 by AFF_1:def_1;
assume LIN o9,b19,a29 ; ::_thesis: contradiction
then a29 in N9 by A7, A8, A16, A20, AFF_1:25;
hence contradiction by A7, A12, A15, A20, A38, AFF_1:25; ::_thesis: verum
end;
assume b2 = b3 ; ::_thesis: contradiction
then a1,b1 // a2,b1 by A6, A11, A18, A19, ANALMETR:60;
then b1,a2 // b1,a1 by ANALMETR:59;
then A39: b19,a29 // b19,a19 by ANALMETR:36;
o9,a29 // o9,a19 by A3, A4, A5, A21, AFF_1:39, AFF_1:41;
then LIN o9,a29,a19 by AFF_1:def_1;
hence contradiction by A29, A37, A39, AFF_1:14; ::_thesis: verum
end;
A40: not LIN b2,a3,b3
proof
assume LIN b2,a3,b3 ; ::_thesis: contradiction
then LIN b29,a39,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A9, A10, A12, A36, A33, AFF_1:25; ::_thesis: verum
end;
A41: a3 <> b3
proof
assume a3 = b3 ; ::_thesis: contradiction
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
b29,b39 // b29,b19 by A8, A9, A10, A33, AFF_1:39, AFF_1:41;
then b2,b3 // b2,b1 by ANALMETR:36;
then A42: LIN b2,b3,b1 by ANALMETR:def_10;
M is being_line by A13, ANALMETR:44;
then A43: M9 is being_line by ANALMETR:43;
then o9,a39 // o9,a19 by A3, A4, A6, AFF_1:39, AFF_1:41;
then A44: o,a3 // o,a1 by ANALMETR:36;
then A45: LIN o,a3,a1 by ANALMETR:def_10;
A46: not LIN a3,a1,b2
proof
assume LIN a3,a1,b2 ; ::_thesis: contradiction
then LIN a39,a19,b29 by ANALMETR:40;
hence contradiction by A4, A6, A11, A30, A43, AFF_1:25; ::_thesis: verum
end;
A47: a3 <> b2
proof
assume a3 = b2 ; ::_thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
A48: o,a3 _|_ o,b3 by A3, A6, A7, A10, A13, ANALMETR:56;
not o,e1 // d1,e2
proof
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
assume o,e1 // d1,e2 ; ::_thesis: contradiction
then o9,e19 // d19,e29 by ANALMETR:36;
then d19,e29 // o9,e19 by AFF_1:4;
then d1,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ a1,b3 by A27, A28, ANALMETR:62;
then o,a3 _|_ a1,b3 by A23, A24, ANALMETR:62;
then o,b3 // a1,b3 by A7, A12, A48, ANALMETR:63;
then o9,b39 // a19,b39 by ANALMETR:36;
then b39,o9 // b39,a19 by AFF_1:4;
then LIN b39,o9,a19 by AFF_1:def_1;
then LIN o9,b39,a19 by AFF_1:6;
then A49: o9,b39 // o9,a19 by AFF_1:def_1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then o9,b29 // o9,b39 by AFF_1:def_1;
then o9,b39 // o9,b29 by AFF_1:4;
then o9,a19 // o9,b29 by A17, A49, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def_1;
then LIN a19,o9,b29 by AFF_1:6;
then A50: a19,o9 // a19,b29 by AFF_1:def_1;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def_1;
then a19,b29 // a19,a39 by A14, A50, DIRAF:40;
then LIN a19,b29,a39 by AFF_1:def_1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
then not o9,e19 // d19,e29 by ANALMETR:36;
then consider d29 being Element of (Af X) such that
A51: LIN o9,e19,d29 and
A52: LIN d19,e29,d29 by AFF_1:60;
reconsider d2 = d29 as Element of X by ANALMETR:35;
LIN d1,e2,d2 by A52, ANALMETR:40;
then A53: d1,e2 // d1,d2 by ANALMETR:def_10;
then A54: a1,b3 _|_ d1,d2 by A27, A28, ANALMETR:62;
then A55: d1,d2 _|_ b3,a1 by ANALMETR:61;
LIN o,e1,d2 by A51, ANALMETR:40;
then o,e1 // o,d2 by ANALMETR:def_10;
then A56: o,a3 // o,d2 by A23, A24, ANALMETR:60;
then A57: LIN o,a3,d2 by ANALMETR:def_10;
then A58: LIN o9,a39,d29 by ANALMETR:40;
consider e1 being Element of X such that
A59: o,b3 // o,e1 and
A60: o <> e1 by ANALMETR:39;
consider e2 being Element of X such that
A61: b3,a3 _|_ d2,e2 and
A62: d2 <> e2 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
not o,e1 // d2,e2
proof
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
assume o,e1 // d2,e2 ; ::_thesis: contradiction
then o9,e19 // d29,e29 by ANALMETR:36;
then d29,e29 // o9,e19 by AFF_1:4;
then d2,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ b3,a3 by A61, A62, ANALMETR:62;
then o,b3 _|_ b3,a3 by A59, A60, ANALMETR:62;
then b3,a3 // o,a3 by A17, A48, ANALMETR:63;
then b39,a39 // o9,a39 by ANALMETR:36;
then a39,b39 // a39,o9 by AFF_1:4;
then LIN a39,b39,o9 by AFF_1:def_1;
then LIN b39,o9,a39 by AFF_1:6;
then A63: b39,o9 // b39,a39 by AFF_1:def_1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def_1;
then b39,a39 // b39,b29 by A17, A63, DIRAF:40;
then LIN b39,a39,b29 by AFF_1:def_1;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
then not o9,e19 // d29,e29 by ANALMETR:36;
then consider d39 being Element of (Af X) such that
A64: LIN o9,e19,d39 and
A65: LIN d29,e29,d39 by AFF_1:60;
reconsider d3 = d39 as Element of X by ANALMETR:35;
LIN d2,e2,d3 by A65, ANALMETR:40;
then A66: d2,e2 // d2,d3 by ANALMETR:def_10;
then A67: b3,a3 _|_ d2,d3 by A61, A62, ANALMETR:62;
then d2,d3 _|_ a3,b3 by ANALMETR:61;
then A68: d2,d3 _|_ a1,b1 by A19, A41, ANALMETR:62;
LIN o,e1,d3 by A64, ANALMETR:40;
then o,e1 // o,d3 by ANALMETR:def_10;
then A69: o,b3 // o,d3 by A59, A60, ANALMETR:60;
then A70: LIN o,b3,d3 by ANALMETR:def_10;
then A71: LIN o9,b39,d39 by ANALMETR:40;
consider e2 being Element of X such that
A72: a3,b2 _|_ d3,e2 and
A73: d3 <> e2 by ANALMETR:39;
consider e1 being Element of X such that
A74: o,a3 // o,e1 and
A75: o <> e1 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
not o,e1 // d3,e2
proof
reconsider e19 = e1, e29 = e2 as Element of (Af X) by ANALMETR:35;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b29,o9,b39 by AFF_1:6;
then A76: b29,o9 // b29,b39 by AFF_1:def_1;
assume o,e1 // d3,e2 ; ::_thesis: contradiction
then o9,e19 // d39,e29 by ANALMETR:36;
then d39,e29 // o9,e19 by AFF_1:4;
then d3,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ a3,b2 by A72, A73, ANALMETR:62;
then o,a3 _|_ a3,b2 by A74, A75, ANALMETR:62;
then A77: o,b3 // a3,b2 by A7, A12, A48, ANALMETR:63;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN o9,b39,b29 by AFF_1:6;
then LIN o,b3,b2 by ANALMETR:40;
then o,b3 // o,b2 by ANALMETR:def_10;
then o,b2 // a3,b2 by A17, A77, ANALMETR:60;
then o9,b29 // a39,b29 by ANALMETR:36;
then b29,o9 // b29,a39 by AFF_1:4;
then b29,a39 // b29,b39 by A3, A11, A76, DIRAF:40;
then LIN b29,a39,b39 by AFF_1:def_1;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
then not o9,e19 // d39,e29 by ANALMETR:36;
then consider d49 being Element of (Af X) such that
A78: LIN o9,e19,d49 and
A79: LIN d39,e29,d49 by AFF_1:60;
reconsider d4 = d49 as Element of X by ANALMETR:35;
LIN d3,e2,d4 by A79, ANALMETR:40;
then A80: d3,e2 // d3,d4 by ANALMETR:def_10;
then A81: d3,d4 _|_ a3,b2 by A72, A73, ANALMETR:62;
LIN o,e1,d4 by A78, ANALMETR:40;
then o,e1 // o,d4 by ANALMETR:def_10;
then A82: o,a3 // o,d4 by A74, A75, ANALMETR:60;
then A83: LIN o,a3,d4 by ANALMETR:def_10;
then A84: LIN o9,a39,d49 by ANALMETR:40;
A85: a3,b2 _|_ d3,d4 by A72, A73, A80, ANALMETR:62;
then ( d3,d4 _|_ a2,b1 or a3 = b2 ) by A18, ANALMETR:62;
then A86: d3,d4 _|_ b1,a2 by A47, ANALMETR:61;
A87: d2 <> o
proof
o,a3 _|_ o,d1 by A17, A48, A25, ANALMETR:62;
then A88: d1,o _|_ o,a3 by ANALMETR:61;
assume d2 = o ; ::_thesis: contradiction
then d1,o _|_ a1,b3 by A27, A28, A53, ANALMETR:62;
then o,a3 // a1,b3 by A26, A88, ANALMETR:63;
then a1,b3 // o,a1 by A7, A12, A44, ANALMETR:60;
then a19,b39 // o9,a19 by ANALMETR:36;
then a19,b39 // a19,o9 by AFF_1:4;
then LIN a19,b39,o9 by AFF_1:def_1;
then LIN o9,b39,a19 by AFF_1:6;
then A89: o9,b39 // o9,a19 by AFF_1:def_1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN o9,b39,b29 by AFF_1:6;
then o9,b39 // o9,b29 by AFF_1:def_1;
then o9,a19 // o9,b29 by A17, A89, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def_1;
then LIN a19,o9,b29 by AFF_1:6;
then A90: a19,o9 // a19,b29 by AFF_1:def_1;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def_1;
then a19,b29 // a19,a39 by A14, A90, DIRAF:40;
then LIN a19,b29,a39 by AFF_1:def_1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
A91: not LIN d1,d2,d3
proof
A92: d2 <> d3
proof
assume d2 = d3 ; ::_thesis: contradiction
then o9,b39 // o9,d29 by A69, ANALMETR:36;
then o9,d29 // o9,b39 by AFF_1:4;
then o,d2 // o,b3 by ANALMETR:36;
then o,b3 // o,a3 by A56, A87, ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def_1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def_1;
then A93: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def_1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17, A93, ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def_10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
A94: d1 <> d2
proof
assume d1 = d2 ; ::_thesis: contradiction
then o9,a39 // o9,d19 by A56, ANALMETR:36;
then o9,d19 // o9,a39 by AFF_1:4;
then o,d1 // o,a3 by ANALMETR:36;
then o,b3 // o,a3 by A25, A26, ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def_1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def_1;
then A95: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def_1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17, A95, ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def_10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
assume LIN d1,d2,d3 ; ::_thesis: contradiction
then LIN d19,d29,d39 by ANALMETR:40;
then LIN d29,d19,d39 by AFF_1:6;
then d29,d19 // d29,d39 by AFF_1:def_1;
then d19,d29 // d29,d39 by AFF_1:4;
then d1,d2 // d2,d3 by ANALMETR:36;
then d2,d3 _|_ a1,b3 by A54, A94, ANALMETR:62;
then a1,b3 // b3,a3 by A67, A92, ANALMETR:63;
then a19,b39 // b39,a39 by ANALMETR:36;
then b39,a19 // b39,a39 by AFF_1:4;
then LIN b39,a19,a39 by AFF_1:def_1;
then LIN a19,a39,b39 by AFF_1:6;
then a19,a39 // a19,b39 by AFF_1:def_1;
then A96: a1,a3 // a1,b3 by ANALMETR:36;
A97: a1 <> a3
proof
assume a1 = a3 ; ::_thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,a39,o9 by AFF_1:6;
then a19,a39 // a19,o9 by AFF_1:def_1;
then a1,a3 // a1,o by ANALMETR:36;
then a1,o // a1,b3 by A97, A96, ANALMETR:60;
then LIN a1,o,b3 by ANALMETR:def_10;
then LIN a19,o9,b39 by ANALMETR:40;
then LIN o9,b39,a19 by AFF_1:6;
then A98: o9,b39 // o9,a19 by AFF_1:def_1;
o9,b39 // o9,b29 by A34, AFF_1:4;
then o9,a19 // o9,b29 by A17, A98, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def_1;
then LIN a19,o9,b29 by AFF_1:6;
then a19,o9 // a19,b29 by AFF_1:def_1;
then A99: a1,o // a1,b2 by ANALMETR:36;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def_1;
then a1,o // a1,a3 by ANALMETR:36;
then a1,b2 // a1,a3 by A14, A99, ANALMETR:60;
then LIN a1,b2,a3 by ANALMETR:def_10;
then LIN a19,b29,a39 by ANALMETR:40;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
A100: d2 <> d4
proof
A101: d2 <> d3
proof
assume d2 = d3 ; ::_thesis: contradiction
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91, ANALMETR:40; ::_thesis: verum
end;
assume d2 = d4 ; ::_thesis: contradiction
then a3,b2 _|_ d2,d3 by A85, ANALMETR:61;
then a3,b2 // b3,a3 by A67, A101, ANALMETR:63;
then a3,b2 // a3,b3 by ANALMETR:59;
then LIN a3,b2,b3 by ANALMETR:def_10;
then LIN a39,b29,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A9, A10, A12, A20, A36, AFF_1:25; ::_thesis: verum
end;
LIN o9,b39,b39 by AFF_1:7;
then A102: LIN d19,d39,b39 by A17, A32, A71, AFF_1:8;
then consider A9 being Subset of (Af X) such that
A103: A9 is being_line and
A104: d19 in A9 and
A105: d39 in A9 and
A106: b39 in A9 by AFF_1:21;
reconsider A = A9 as Subset of X by ANALMETR:42;
A107: d19 <> d39
proof
assume d19 = d39 ; ::_thesis: contradiction
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91, ANALMETR:40; ::_thesis: verum
end;
then A9 = Line (d19,d39) by A103, A104, A105, AFF_1:24;
then A108: A = Line (d1,d3) by ANALMETR:41;
LIN o9,b29,b39 by A35, ANALMETR:40;
then A109: LIN o9,b39,b29 by AFF_1:6;
then A110: b2 in A by A17, A32, A71, A103, A104, A105, A107, AFF_1:8, AFF_1:25;
A111: o <> d3
proof
assume d3 = o ; ::_thesis: contradiction
then A112: d2,o _|_ b3,a3 by A61, A62, A66, ANALMETR:62;
o,b3 _|_ o,d2 by A7, A12, A48, A56, ANALMETR:62;
then d2,o _|_ o,b3 by ANALMETR:61;
then o,b3 // b3,a3 by A87, A112, ANALMETR:63;
then o9,b39 // b39,a39 by ANALMETR:36;
then A113: b39,o9 // b39,a39 by AFF_1:4;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def_1;
then b39,a39 // b39,b29 by A17, A113, DIRAF:40;
then LIN b39,a39,b29 by AFF_1:def_1;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
A114: o <> d4
proof
o,a3 _|_ o,d3 by A17, A48, A69, ANALMETR:62;
then A115: d3,o _|_ o,a3 by ANALMETR:61;
assume d4 = o ; ::_thesis: contradiction
then d3,o _|_ a3,b2 by A72, A73, A80, ANALMETR:62;
then o,a3 // a3,b2 by A111, A115, ANALMETR:63;
then o9,a39 // a39,b29 by ANALMETR:36;
then A116: a39,o9 // a39,b29 by AFF_1:4;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a39,o9,a19 by AFF_1:6;
then a39,o9 // a39,a19 by AFF_1:def_1;
then a39,b29 // a39,a19 by A7, A12, A116, DIRAF:40;
then LIN a39,b29,a19 by AFF_1:def_1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
A117: not LIN d1,d4,d3
proof
A118: d1 <> d3
proof
A119: d1 <> d2
proof
assume d1 = d2 ; ::_thesis: contradiction
then o9,a39 // o9,d19 by A56, ANALMETR:36;
then o9,d19 // o9,a39 by AFF_1:4;
then o,d1 // o,a3 by ANALMETR:36;
then o,b3 // o,a3 by A25, A26, ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def_1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def_1;
then A120: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def_1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17, A120, ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def_10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
assume d1 = d3 ; ::_thesis: contradiction
then a3,b3 _|_ d1,d2 by A67, ANALMETR:61;
then a1,b3 // a3,b3 by A54, A119, ANALMETR:63;
then a19,b39 // a39,b39 by ANALMETR:36;
then b39,a19 // b39,a39 by AFF_1:4;
then LIN b39,a19,a39 by AFF_1:def_1;
then LIN a19,a39,b39 by AFF_1:6;
then a19,a39 // a19,b39 by AFF_1:def_1;
then A121: a1,a3 // a1,b3 by ANALMETR:36;
A122: a1 <> a3
proof
assume a1 = a3 ; ::_thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,a39,o9 by AFF_1:6;
then a19,a39 // a19,o9 by AFF_1:def_1;
then a1,a3 // a1,o by ANALMETR:36;
then a1,o // a1,b3 by A122, A121, ANALMETR:60;
then LIN a1,o,b3 by ANALMETR:def_10;
then LIN a19,o9,b39 by ANALMETR:40;
then LIN o9,b39,a19 by AFF_1:6;
then A123: o9,b39 // o9,a19 by AFF_1:def_1;
o9,b39 // o9,b29 by A34, AFF_1:4;
then o9,a19 // o9,b29 by A17, A123, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def_1;
then LIN a19,o9,b29 by AFF_1:6;
then a19,o9 // a19,b29 by AFF_1:def_1;
then A124: a1,o // a1,b2 by ANALMETR:36;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def_1;
then a1,o // a1,a3 by ANALMETR:36;
then a1,b2 // a1,a3 by A14, A124, ANALMETR:60;
then LIN a1,b2,a3 by ANALMETR:def_10;
then LIN a19,b29,a39 by ANALMETR:40;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
assume LIN d1,d4,d3 ; ::_thesis: contradiction
then LIN d19,d49,d39 by ANALMETR:40;
then A125: LIN d19,d39,d49 by AFF_1:6;
A126: b29 <> b39
proof
assume b29 = b39 ; ::_thesis: contradiction
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b29,b39,o9 by AFF_1:6;
then A127: b29,b39 // b29,o9 by AFF_1:def_1;
LIN d19,d39,b29 by A17, A32, A71, A109, AFF_1:8;
then LIN b29,b39,d49 by A102, A118, A125, AFF_1:8;
then b29,b39 // b29,d49 by AFF_1:def_1;
then b29,o9 // b29,d49 by A127, A126, DIRAF:40;
then LIN b29,o9,d49 by AFF_1:def_1;
then LIN o9,d49,b29 by AFF_1:6;
then A128: o9,d49 // o9,b29 by AFF_1:def_1;
o9,a39 // o9,d49 by A82, ANALMETR:36;
then o9,d49 // o9,a39 by AFF_1:4;
then o9,b29 // o9,a39 by A114, A128, DIRAF:40;
then LIN o9,b29,a39 by AFF_1:def_1;
then LIN b29,o9,a39 by AFF_1:6;
then A129: b29,o9 // b29,a39 by AFF_1:def_1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b29,o9,b39 by AFF_1:6;
then b29,o9 // b29,b39 by AFF_1:def_1;
then b29,a39 // b29,b39 by A3, A11, A129, DIRAF:40;
then LIN b29,a39,b39 by AFF_1:def_1;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
A130: not d4 in A
proof
assume d4 in A ; ::_thesis: contradiction
then d19,d49 // d19,d39 by A103, A104, A105, AFF_1:39, AFF_1:41;
then LIN d19,d49,d39 by AFF_1:def_1;
hence contradiction by A117, ANALMETR:40; ::_thesis: verum
end;
A131: d2,d3 _|_ b3,a3 by A61, A62, A66, ANALMETR:62;
take d4 = d4; ::_thesis: a1,b2 // a2,b3
LIN o9,b39,d19 by A31, ANALMETR:40;
then A132: o9,b39 // o9,d19 by AFF_1:def_1;
LIN o9,a39,a19 by A45, ANALMETR:40;
then A133: LIN d29,d49,a19 by A7, A12, A58, A84, AFF_1:8;
then consider K9 being Subset of (Af X) such that
A134: K9 is being_line and
A135: d29 in K9 and
A136: d49 in K9 and
A137: a19 in K9 by AFF_1:21;
reconsider K = K9 as Subset of X by ANALMETR:42;
LIN o9,a39,a39 by AFF_1:7;
then A138: a3 in K by A7, A12, A58, A84, A100, A134, A135, A136, AFF_1:8, AFF_1:25;
a39,a19 // a39,a29 by A4, A5, A6, A43, AFF_1:39, AFF_1:41;
then a3,a1 // a3,a2 by ANALMETR:36;
then A139: LIN a3,a1,a2 by ANALMETR:def_10;
A140: ( LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2 )
proof
A141: b39 <> b29
proof
assume b39 = b29 ; ::_thesis: contradiction
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40, ANALMETR:40; ::_thesis: verum
end;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,b29,o9 by AFF_1:6;
then A142: b39,b29 // b39,o9 by AFF_1:def_1;
LIN b29,b39,b19 by A42, ANALMETR:40;
then LIN b39,b29,b19 by AFF_1:6;
then b39,b29 // b39,b19 by AFF_1:def_1;
then b39,b19 // b39,o9 by A142, A141, DIRAF:40;
then LIN b39,b19,o9 by AFF_1:def_1;
then A143: LIN o9,b39,b19 by AFF_1:6;
A144: LIN o9,b39,d39 by A70, ANALMETR:40;
LIN o9,b39,d19 by A31, ANALMETR:40;
then A145: LIN d19,d39,b19 by A17, A143, A144, AFF_1:8;
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, d29 = d2, d49 = d4 as Element of (Af X) by ANALMETR:35;
A146: a39 <> a19
proof
assume a19 = a39 ; ::_thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a39,a19,o9 by AFF_1:6;
then A147: a39,a19 // a39,o9 by AFF_1:def_1;
LIN a39,a19,a29 by A139, ANALMETR:40;
then a39,a19 // a39,a29 by AFF_1:def_1;
then a39,a29 // a39,o9 by A147, A146, DIRAF:40;
then LIN a39,a29,o9 by AFF_1:def_1;
then A148: LIN o9,a39,a29 by AFF_1:6;
A149: LIN o9,a39,d49 by A83, ANALMETR:40;
LIN o9,a39,d29 by A57, ANALMETR:40;
then LIN d29,d49,a29 by A7, A12, A148, A149, AFF_1:8;
hence ( LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2 ) by A102, A133, A145, ANALMETR:40; ::_thesis: verum
end;
LIN o9,b39,d39 by A70, ANALMETR:40;
then o9,b39 // o9,d39 by AFF_1:def_1;
then o9,d19 // o9,d39 by A17, A132, DIRAF:40;
then LIN o9,d19,d39 by AFF_1:def_1;
then LIN d19,o9,d39 by AFF_1:6;
then d19,o9 // d19,d39 by AFF_1:def_1;
then o9,d19 // d19,d39 by AFF_1:4;
then A150: o,d1 // d1,d3 by ANALMETR:36;
o,b3 // o,d1 by A132, ANALMETR:36;
then o,d1 _|_ o,a3 by A17, A48, ANALMETR:62;
then A151: o,a3 _|_ d1,d3 by A26, A150, ANALMETR:62;
LIN o9,a39,d29 by A57, ANALMETR:40;
then A152: o9,a39 // o9,d29 by AFF_1:def_1;
then o,a3 // o,d2 by ANALMETR:36;
then A153: o,d2 _|_ d1,d3 by A7, A12, A151, ANALMETR:62;
A154: not d2 in A
proof
assume d2 in A ; ::_thesis: contradiction
then d19,d29 // d19,d39 by A103, A104, A105, AFF_1:39, AFF_1:41;
then LIN d19,d29,d39 by AFF_1:def_1;
hence contradiction by A91, ANALMETR:40; ::_thesis: verum
end;
LIN o9,a39,d49 by A83, ANALMETR:40;
then o9,a39 // o9,d49 by AFF_1:def_1;
then o9,d29 // o9,d49 by A7, A12, A152, DIRAF:40;
then LIN o9,d29,d49 by AFF_1:def_1;
then LIN d29,o9,d49 by AFF_1:6;
then d29,o9 // d29,d49 by AFF_1:def_1;
then o9,d29 // d29,d49 by AFF_1:4;
then o,d2 // d2,d4 by ANALMETR:36;
then A155: d1,d3 _|_ d2,d4 by A87, A153, ANALMETR:62;
K9 = Line (d29,d49) by A100, A134, A135, A136, AFF_1:24;
then K = Line (d2,d4) by ANALMETR:41;
then A156: A _|_ K by A155, A100, A107, A108, ANALMETR:45;
reconsider d19 = d1, d29 = d2, d39 = d3, d49 = d4, b39 = b3, a19 = a1, b19 = b1, a29 = a2 as Element of (Af X) by ANALMETR:35;
LIN d19,d39,b39 by A140, ANALMETR:40;
then consider A9 being Subset of (Af X) such that
A157: A9 is being_line and
A158: d19 in A9 and
A159: d39 in A9 and
A160: b39 in A9 by AFF_1:21;
A161: d19 <> d39
proof
assume d19 = d39 ; ::_thesis: contradiction
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91, ANALMETR:40; ::_thesis: verum
end;
reconsider A = A9 as Subset of X by ANALMETR:42;
LIN d19,d39,b19 by A140, ANALMETR:40;
then A162: b1 in A by A157, A158, A159, A161, AFF_1:25;
A163: not d2 in A
proof
assume d2 in A ; ::_thesis: contradiction
then d19,d29 // d19,d39 by A157, A158, A159, AFF_1:39, AFF_1:41;
then d1,d2 // d1,d3 by ANALMETR:36;
hence contradiction by A91, ANALMETR:def_10; ::_thesis: verum
end;
A164: d1 <> d4
proof
LIN o9,a39,d49 by A83, ANALMETR:40;
then A165: LIN o9,d49,a39 by AFF_1:6;
LIN o9,d49,o9 by AFF_1:7;
then A166: o9,d49 // o9,a39 by A165, AFF_1:10;
A167: LIN o9,b39,o9 by AFF_1:7;
LIN o9,b29,b39 by A35, ANALMETR:40;
then A168: LIN o9,b39,b29 by AFF_1:6;
LIN o9,b39,d19 by A31, ANALMETR:40;
then LIN o9,d19,b29 by A17, A167, A168, AFF_1:8;
then A169: o9,d19 // o9,b29 by AFF_1:def_1;
assume d1 = d4 ; ::_thesis: contradiction
then o9,a39 // o9,b29 by A114, A169, A166, DIRAF:40;
then LIN o9,a39,b29 by AFF_1:def_1;
then LIN a39,b29,o9 by AFF_1:6;
then a39,b29 // a39,o9 by AFF_1:def_1;
then A170: a39,o9 // a39,b29 by AFF_1:4;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a39,o9,a19 by AFF_1:6;
then a39,o9 // a39,a19 by AFF_1:def_1;
then a39,b29 // a39,a19 by A7, A12, A170, DIRAF:40;
then LIN a39,b29,a19 by AFF_1:def_1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; ::_thesis: verum
end;
A171: not d4 in A
proof
assume d4 in A ; ::_thesis: contradiction
then d19,d49 // d19,d39 by A157, A158, A159, AFF_1:39, AFF_1:41;
then d1,d4 // d1,d3 by ANALMETR:36;
hence contradiction by A117, ANALMETR:def_10; ::_thesis: verum
end;
LIN d29,d49,a19 by A140, ANALMETR:40;
then consider K9 being Subset of (Af X) such that
A172: K9 is being_line and
A173: d29 in K9 and
A174: d49 in K9 and
A175: a19 in K9 by AFF_1:21;
reconsider K = K9 as Subset of X by ANALMETR:42;
LIN d29,d49,a29 by A140, ANALMETR:40;
then A176: a2 in K by A100, A172, A173, A174, AFF_1:25;
K9 = Line (d29,d49) by A100, A172, A173, A174, AFF_1:24;
then A177: K = Line (d2,d4) by ANALMETR:41;
A9 = Line (d19,d39) by A157, A158, A159, A161, AFF_1:24;
then A = Line (d1,d3) by ANALMETR:41;
then A _|_ K by A155, A100, A161, A177, ANALMETR:45;
then A178: d1,d4 _|_ b3,a2 by A1, A68, A86, A55, A158, A159, A160, A173, A174, A175, A163, A171, A162, A176, Def3;
d1,d2 _|_ a1,b3 by A27, A28, A53, ANALMETR:62;
then d1,d4 _|_ a1,b2 by A2, A131, A81, A104, A105, A106, A135, A136, A137, A154, A130, A156, A110, A138, Def4;
then ( a1,b2 // b3,a2 or d1 = d4 ) by A178, ANALMETR:63;
then a19,b29 // b39,a29 by A164, ANALMETR:36;
then a19,b29 // a29,b39 by AFF_1:4;
hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum
end;
now__::_thesis:_(_(_a1_=_a2_or_a2_=_a3_or_a1_=_a3_)_implies_a1,b2_//_a2,b3_)
A179: now__::_thesis:_(_a1_=_a2_implies_a1,b2_//_a2,b3_)
o9,b29 // o9,b39 by A7, A9, A10, A20, AFF_1:39, AFF_1:41;
then A180: LIN o9,b29,b39 by AFF_1:def_1;
assume A181: a1 = a2 ; ::_thesis: a1,b2 // a2,b3
a1 <> b1
proof
o9,a19 // o9,a39 by A3, A4, A6, A21, AFF_1:39, AFF_1:41;
then A182: LIN o9,a19,a39 by AFF_1:def_1;
assume a1 = b1 ; ::_thesis: contradiction
hence contradiction by A7, A8, A12, A14, A20, A182, AFF_1:25; ::_thesis: verum
end;
then a3,b2 // a3,b3 by A18, A19, A181, ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29 = b39 by A3, A6, A7, A11, A12, A21, A180, AFF_1:14, AFF_1:25;
then a19,b29 // a29,b39 by A181, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum
end;
A183: now__::_thesis:_(_a1_=_a3_implies_a1,b2_//_a2,b3_)
A184: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19 ; ::_thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; ::_thesis: verum
end;
o9,b19 // o9,b39 by A7, A8, A10, A20, AFF_1:39, AFF_1:41;
then A185: LIN o9,b19,b39 by AFF_1:def_1;
assume A186: a1 = a3 ; ::_thesis: a1,b2 // a2,b3
then a3,b1 // a3,b3 by A19, ANALMETR:59;
then a39,b19 // a39,b39 by ANALMETR:36;
hence a1,b2 // a2,b3 by A18, A186, A184, A185, AFF_1:14; ::_thesis: verum
end;
A187: now__::_thesis:_(_a2_=_a3_implies_a1,b2_//_a2,b3_)
A188: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19 ; ::_thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; ::_thesis: verum
end;
o9,b19 // o9,b29 by A7, A8, A9, A20, AFF_1:39, AFF_1:41;
then A189: LIN o9,b19,b29 by AFF_1:def_1;
assume A190: a2 = a3 ; ::_thesis: a1,b2 // a2,b3
then a3,b1 // a3,b2 by A18, ANALMETR:59;
then a39,b19 // a39,b29 by ANALMETR:36;
then a2,b3 // a1,b2 by A19, A190, A188, A189, AFF_1:14;
hence a1,b2 // a2,b3 by ANALMETR:59; ::_thesis: verum
end;
assume ( a1 = a2 or a2 = a3 or a1 = a3 ) ; ::_thesis: a1,b2 // a2,b3
hence a1,b2 // a2,b3 by A179, A187, A183; ::_thesis: verum
end;
hence a1,b2 // a2,b3 by A22; ::_thesis: verum
end;
theorem :: CONMETR:15
for X being OrtAfPl st X is satisfying_3H holds
X is satisfying_OPAP
proof
let X be OrtAfPl; ::_thesis: ( X is satisfying_3H implies X is satisfying_OPAP )
assume A1: X is satisfying_3H ; ::_thesis: X is satisfying_OPAP
let o be Element of X; :: according to CONMETR:def_1 ::_thesis: for a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let a1, a2, a3, b1, b2, b3 be Element of X; ::_thesis: for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds
a1,b2 // a2,b3
let M, N be Subset of X; ::_thesis: ( o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )
assume that
A2: o in M and
A3: a1 in M and
A4: a2 in M and
A5: a3 in M and
A6: o in N and
A7: b1 in N and
A8: b2 in N and
A9: b3 in N and
A10: not b2 in M and
A11: not a3 in N and
A12: M _|_ N and
A13: o <> a1 and
A14: o <> a2 and
o <> a3 and
A15: o <> b1 and
o <> b2 and
A16: o <> b3 and
A17: a3,b2 // a2,b1 and
A18: a3,b3 // a1,b1 ; ::_thesis: a1,b2 // a2,b3
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of (Af X) by ANALMETR:35;
reconsider M9 = M, N9 = N as Subset of (Af X) by ANALMETR:42;
N is being_line by A12, ANALMETR:44;
then A19: N9 is being_line by ANALMETR:43;
M is being_line by A12, ANALMETR:44;
then A20: M9 is being_line by ANALMETR:43;
A21: now__::_thesis:_(_b2_=_b3_implies_a1,b2_//_a2,b3_)
A22: not LIN o9,b19,a19
proof
o9,a19 // o9,a39 by A2, A3, A5, A20, AFF_1:39, AFF_1:41;
then A23: LIN o9,a19,a39 by AFF_1:def_1;
assume LIN o9,b19,a19 ; ::_thesis: contradiction
then a19 in N9 by A6, A7, A15, A19, AFF_1:25;
hence contradiction by A6, A11, A13, A19, A23, AFF_1:25; ::_thesis: verum
end;
A24: b1,a2 // a3,b2 by A17, ANALMETR:59;
o9,a19 // o9,a29 by A2, A3, A4, A20, AFF_1:39, AFF_1:41;
then A25: LIN o9,a19,a29 by AFF_1:def_1;
assume A26: b2 = b3 ; ::_thesis: a1,b2 // a2,b3
then b1,a1 // a3,b2 by A18, ANALMETR:59;
then b1,a1 // b1,a2 by A5, A10, A24, ANALMETR:60;
then b19,a19 // b19,a29 by ANALMETR:36;
then a19 = a29 by A22, A25, AFF_1:14;
then a19,b29 // a29,b39 by A26, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum
end;
A27: for a, b, c being Element of X st LIN a,b,c holds
( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )
proof
let a, b, c be Element of X; ::_thesis: ( LIN a,b,c implies ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) )
reconsider a9 = a, b9 = b, c9 = c as Element of (Af X) by ANALMETR:35;
assume LIN a,b,c ; ::_thesis: ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )
then A28: LIN a9,b9,c9 by ANALMETR:40;
then A29: LIN b9,a9,c9 by AFF_1:6;
A30: LIN c9,a9,b9 by A28, AFF_1:6;
A31: LIN b9,c9,a9 by A28, AFF_1:6;
A32: LIN c9,b9,a9 by A28, AFF_1:6;
LIN a9,c9,b9 by A28, AFF_1:6;
hence ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) by A29, A31, A30, A32, ANALMETR:40; ::_thesis: verum
end;
A33: now__::_thesis:_(_a1_<>_a3_&_b2_<>_b3_implies_a1,b2_//_a2,b3_)
o9,a39 // o9,a19 by A2, A3, A5, A20, AFF_1:39, AFF_1:41;
then LIN o9,a39,a19 by AFF_1:def_1;
then A34: LIN o,a3,a1 by ANALMETR:40;
a39,a19 // a39,a29 by A3, A4, A5, A20, AFF_1:39, AFF_1:41;
then LIN a39,a19,a29 by AFF_1:def_1;
then A35: LIN a3,a1,a2 by ANALMETR:40;
o9,b29 // o9,b39 by A6, A8, A9, A19, AFF_1:39, AFF_1:41;
then LIN o9,b29,b39 by AFF_1:def_1;
then A36: LIN o,b2,b3 by ANALMETR:40;
assume that
A37: a1 <> a3 and
A38: b2 <> b3 ; ::_thesis: a1,b2 // a2,b3
A39: ( not LIN a3,a1,b2 & not LIN b2,a3,b3 )
proof
assume ( LIN a3,a1,b2 or LIN b2,a3,b3 ) ; ::_thesis: contradiction
then ( LIN a39,a19,b29 or LIN b29,a39,b39 ) by ANALMETR:40;
then ( LIN a39,a19,b29 or LIN b29,b39,a39 ) by AFF_1:6;
hence contradiction by A3, A5, A8, A9, A10, A11, A20, A19, A37, A38, AFF_1:25; ::_thesis: verum
end;
b29,b39 // b29,b19 by A7, A8, A9, A19, AFF_1:39, AFF_1:41;
then LIN b29,b39,b19 by AFF_1:def_1;
then A40: LIN b2,b3,b1 by ANALMETR:40;
A41: now__::_thesis:_(_b2_<>_b1_implies_a1,b2_//_a2,b3_)
assume A42: b2 <> b1 ; ::_thesis: a1,b2 // a2,b3
not LIN a2,a3,b3
proof
A43: a3 <> a2
proof
assume a3 = a2 ; ::_thesis: contradiction
then LIN a3,b2,b1 by A17, ANALMETR:def_10;
then LIN b2,b1,a3 by A27;
then A44: b2,b1 // b2,a3 by ANALMETR:def_10;
LIN b2,b1,b3 by A27, A40;
then b2,b1 // b2,b3 by ANALMETR:def_10;
then b2,a3 // b2,b3 by A42, A44, ANALMETR:60;
hence contradiction by A39, ANALMETR:def_10; ::_thesis: verum
end;
LIN a3,a1,o by A27, A34;
then A45: a3,a1 // a3,o by ANALMETR:def_10;
A46: a3 <> a1
proof
assume a3 = a1 ; ::_thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A39, ANALMETR:40; ::_thesis: verum
end;
assume LIN a2,a3,b3 ; ::_thesis: contradiction
then LIN a3,a2,b3 by A27;
then A47: a3,a2 // a3,b3 by ANALMETR:def_10;
LIN a3,a2,a1 by A27, A35;
then a3,a2 // a3,a1 by ANALMETR:def_10;
then a3,a1 // a3,b3 by A47, A43, ANALMETR:60;
then a3,o // a3,b3 by A46, A45, ANALMETR:60;
then a39,o9 // a39,b39 by ANALMETR:36;
then A48: a39,b39 // a39,o9 by AFF_1:4;
LIN b2,b3,o by A27, A36;
then A49: LIN b29,b39,o9 by ANALMETR:40;
not LIN b29,a39,b39 by A39, ANALMETR:40;
hence contradiction by A16, A48, A49, AFF_1:14; ::_thesis: verum
end;
then consider c1 being Element of X such that
A50: c1,a2 _|_ a3,b3 and
A51: c1,a3 _|_ a2,b3 and
A52: c1,b3 _|_ a2,a3 by A1, CONAFFM:def_3;
reconsider c19 = c1 as Element of (Af X) by ANALMETR:35;
A53: now__::_thesis:_(_a2_<>_a1_implies_a1,b2_//_a2,b3_)
A54: a2 <> a3
proof
A55: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19 ; ::_thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; ::_thesis: verum
end;
assume a2 = a3 ; ::_thesis: contradiction
then a39,b29 // a39,b19 by A17, ANALMETR:36;
then A56: a39,b19 // a39,b29 by AFF_1:4;
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then LIN o9,b19,b29 by AFF_1:def_1;
hence contradiction by A42, A55, A56, AFF_1:14; ::_thesis: verum
end;
a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:56;
then b2,b3 // c1,b3 by A52, A54, ANALMETR:63;
then b3,b2 // b3,c1 by ANALMETR:59;
then LIN b3,b2,c1 by ANALMETR:def_10;
then LIN b39,b29,c19 by ANALMETR:40;
then A57: c1 in N by A8, A9, A19, A38, AFF_1:25;
A58: not LIN o9,a29,c19
proof
A59: o9 <> c19
proof
assume A60: o9 = c19 ; ::_thesis: contradiction
o,a2 _|_ b3,b2 by A2, A4, A8, A9, A12, ANALMETR:56;
then b3,b2 // a3,b3 by A14, A50, A60, ANALMETR:63;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def_10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; ::_thesis: verum
end;
o9,a29 // o9,a39 by A2, A4, A5, A20, AFF_1:39, AFF_1:41;
then A61: LIN o9,a29,a39 by AFF_1:def_1;
assume LIN o9,a29,c19 ; ::_thesis: contradiction
then LIN o9,c19,a29 by AFF_1:6;
then a29 in N9 by A6, A19, A57, A59, AFF_1:25;
hence contradiction by A6, A11, A14, A19, A61, AFF_1:25; ::_thesis: verum
end;
A62: a1 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A63: LIN o9,b19,b29 by AFF_1:def_1;
assume a1 = b1 ; ::_thesis: contradiction
hence contradiction by A2, A3, A10, A13, A20, A63, AFF_1:25; ::_thesis: verum
end;
assume A64: a2 <> a1 ; ::_thesis: a1,b2 // a2,b3
A65: a1 <> b1
proof
LIN a1,a2,a3 by A27, A35;
then a1,a2 // a1,a3 by ANALMETR:def_10;
then A66: a2,a1 // a3,a1 by ANALMETR:59;
assume a1 = b1 ; ::_thesis: contradiction
then a3,a1 // a3,b2 by A17, A64, A66, ANALMETR:60;
hence contradiction by A39, ANALMETR:def_10; ::_thesis: verum
end;
not LIN a2,a1,b1
proof
assume LIN a2,a1,b1 ; ::_thesis: contradiction
then LIN b1,a1,a2 by A27;
then b1,a1 // b1,a2 by ANALMETR:def_10;
then a1,b1 // a2,b1 by ANALMETR:59;
then A67: a2,b1 // a3,b3 by A18, A65, ANALMETR:60;
a2 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A68: LIN o9,b19,b29 by AFF_1:def_1;
assume a2 = b1 ; ::_thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A68, AFF_1:25; ::_thesis: verum
end;
then a3,b3 // a3,b2 by A17, A67, ANALMETR:60;
then LIN a3,b3,b2 by ANALMETR:def_10;
hence contradiction by A27, A39; ::_thesis: verum
end;
then consider c2 being Element of X such that
A69: c2,a2 _|_ a1,b1 and
A70: c2,a1 _|_ a2,b1 and
A71: c2,b1 _|_ a2,a1 by A1, CONAFFM:def_3;
reconsider c29 = c2 as Element of (Af X) by ANALMETR:35;
a1,b1 _|_ c1,a2 by A9, A11, A18, A50, ANALMETR:62;
then c2,a2 // c1,a2 by A69, A62, ANALMETR:63;
then a2,c1 // a2,c2 by ANALMETR:59;
then A72: a29,c19 // a29,c29 by ANALMETR:36;
a2,a1 _|_ b1,b2 by A3, A4, A7, A8, A12, ANALMETR:56;
then b1,b2 // c2,b1 by A64, A71, ANALMETR:63;
then b1,b2 // b1,c2 by ANALMETR:59;
then LIN b1,b2,c2 by ANALMETR:def_10;
then LIN b19,b29,c29 by ANALMETR:40;
then A73: c29 in N9 by A7, A8, A19, A42, AFF_1:25;
A74: not LIN o9,a19,c29
proof
A75: o9 <> c29
proof
A76: a2 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A77: LIN o9,b19,b29 by AFF_1:def_1;
assume a2 = b1 ; ::_thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A77, AFF_1:25; ::_thesis: verum
end;
assume o9 = c29 ; ::_thesis: contradiction
then A78: o,a1 _|_ a3,b2 by A17, A70, A76, ANALMETR:62;
o,a1 _|_ b3,b2 by A2, A3, A8, A9, A12, ANALMETR:56;
then b3,b2 // a3,b2 by A13, A78, ANALMETR:63;
then b2,b3 // b2,a3 by ANALMETR:59;
then LIN b2,b3,a3 by ANALMETR:def_10;
then LIN b29,b39,a39 by ANALMETR:40;
hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; ::_thesis: verum
end;
o9,a19 // o9,a39 by A2, A3, A5, A20, AFF_1:39, AFF_1:41;
then A79: LIN o9,a19,a39 by AFF_1:def_1;
assume LIN o9,a19,c29 ; ::_thesis: contradiction
then LIN o9,c29,a19 by AFF_1:6;
then a19 in N9 by A6, A19, A73, A75, AFF_1:25;
hence contradiction by A6, A11, A13, A19, A79, AFF_1:25; ::_thesis: verum
end;
not LIN a3,a1,b2
proof
assume LIN a3,a1,b2 ; ::_thesis: contradiction
then LIN a39,a19,b29 by ANALMETR:40;
hence contradiction by A3, A5, A10, A20, A37, AFF_1:25; ::_thesis: verum
end;
then consider c3 being Element of X such that
A80: c3,a3 _|_ a1,b2 and
A81: c3,a1 _|_ a3,b2 and
A82: c3,b2 _|_ a3,a1 by A1, CONAFFM:def_3;
reconsider c39 = c3 as Element of (Af X) by ANALMETR:35;
a2 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A83: LIN o9,b19,b29 by AFF_1:def_1;
assume a2 = b1 ; ::_thesis: contradiction
hence contradiction by A2, A4, A10, A14, A20, A83, AFF_1:25; ::_thesis: verum
end;
then a3,b2 _|_ c2,a1 by A17, A70, ANALMETR:62;
then c2,a1 // c3,a1 by A5, A10, A81, ANALMETR:63;
then a1,c2 // a1,c3 by ANALMETR:59;
then A84: a19,c29 // a19,c39 by ANALMETR:36;
a2,a1 _|_ b2,b1 by A3, A4, A7, A8, A12, ANALMETR:56;
then b2,b1 // c2,b1 by A64, A71, ANALMETR:63;
then b1,b2 // b1,c2 by ANALMETR:59;
then LIN b1,b2,c2 by ANALMETR:def_10;
then LIN b19,b29,c29 by ANALMETR:40;
then c2 in N by A7, A8, A19, A42, AFF_1:25;
then o9,c19 // o9,c29 by A6, A19, A57, AFF_1:39, AFF_1:41;
then LIN o9,c19,c29 by AFF_1:def_1;
then A85: c1 = c2 by A58, A72, AFF_1:14;
A86: c1 <> a3
proof
A87: a2 <> a3
proof
A88: not LIN o9,a39,b19
proof
assume LIN o9,a39,b19 ; ::_thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; ::_thesis: verum
end;
assume a2 = a3 ; ::_thesis: contradiction
then a39,b29 // a39,b19 by A17, ANALMETR:36;
then A89: a39,b19 // a39,b29 by AFF_1:4;
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then LIN o9,b19,b29 by AFF_1:def_1;
hence contradiction by A42, A88, A89, AFF_1:14; ::_thesis: verum
end;
assume A90: c1 = a3 ; ::_thesis: contradiction
a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:56;
then a3,b3 // b2,b3 by A52, A90, A87, ANALMETR:63;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def_10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; ::_thesis: verum
end;
a3,a1 _|_ b2,b3 by A3, A5, A8, A9, A12, ANALMETR:56;
then c3,b2 // b2,b3 by A37, A82, ANALMETR:63;
then b2,b3 // b2,c3 by ANALMETR:59;
then LIN b2,b3,c3 by ANALMETR:def_10;
then LIN b29,b39,c39 by ANALMETR:40;
then c39 in N9 by A8, A9, A19, A38, AFF_1:25;
then o9,c29 // o9,c39 by A6, A19, A73, AFF_1:39, AFF_1:41;
then LIN o9,c29,c39 by AFF_1:def_1;
then c2 = c3 by A74, A84, AFF_1:14;
hence a1,b2 // a2,b3 by A51, A85, A80, A86, ANALMETR:63; ::_thesis: verum
end;
now__::_thesis:_(_a2_=_a1_implies_a1,b2_//_a2,b3_)
o9,b29 // o9,b39 by A6, A8, A9, A19, AFF_1:39, AFF_1:41;
then A91: LIN o9,b29,b39 by AFF_1:def_1;
assume A92: a2 = a1 ; ::_thesis: a1,b2 // a2,b3
a1 <> b1
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A93: LIN o9,b19,b29 by AFF_1:def_1;
assume a1 = b1 ; ::_thesis: contradiction
hence contradiction by A2, A3, A10, A13, A20, A93, AFF_1:25; ::_thesis: verum
end;
then a3,b2 // a3,b3 by A17, A18, A92, ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29 = b39 by A2, A5, A6, A10, A11, A20, A91, AFF_1:14, AFF_1:25;
then a19,b29 // a29,b39 by A92, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; ::_thesis: verum
end;
hence a1,b2 // a2,b3 by A53; ::_thesis: verum
end;
now__::_thesis:_(_b2_=_b1_implies_a1,b2_//_a2,b3_)
A94: not LIN o9,b29,a39
proof
assume LIN o9,b29,a39 ; ::_thesis: contradiction
then LIN o,b2,a3 by ANALMETR:40;
then LIN b2,o,a3 by A27;
then A95: b2,o // b2,a3 by ANALMETR:def_10;
LIN b2,o,b3 by A27, A36;
then b2,o // b2,b3 by ANALMETR:def_10;
then b2,a3 // b2,b3 by A2, A10, A95, ANALMETR:60;
hence contradiction by A39, ANALMETR:def_10; ::_thesis: verum
end;
LIN a3,a1,o by A27, A34;
then A96: a3,a1 // a3,o by ANALMETR:def_10;
A97: a3 <> a1
proof
assume a3 = a1 ; ::_thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A39, ANALMETR:40; ::_thesis: verum
end;
a3,a1 // a3,a2 by A35, ANALMETR:def_10;
then a3,o // a3,a2 by A96, A97, ANALMETR:60;
then LIN a3,o,a2 by ANALMETR:def_10;
then LIN o,a3,a2 by A27;
then A98: LIN o9,a39,a29 by ANALMETR:40;
assume A99: b2 = b1 ; ::_thesis: a1,b2 // a2,b3
then b2,a3 // b2,a2 by A17, ANALMETR:59;
then b29,a39 // b29,a29 by ANALMETR:36;
then a39 = a29 by A98, A94, AFF_1:14;
hence a1,b2 // a2,b3 by A18, A99, ANALMETR:59; ::_thesis: verum
end;
hence a1,b2 // a2,b3 by A41; ::_thesis: verum
end;
now__::_thesis:_(_a1_=_a3_implies_a1,b2_//_a2,b3_)
A100: not LIN o9,a19,b19
proof
o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;
then A101: LIN o9,b19,b29 by AFF_1:def_1;
assume LIN o9,a19,b19 ; ::_thesis: contradiction
then b19 in M9 by A2, A3, A13, A20, AFF_1:25;
hence contradiction by A2, A10, A15, A20, A101, AFF_1:25; ::_thesis: verum
end;
o9,b19 // o9,b39 by A6, A7, A9, A19, AFF_1:39, AFF_1:41;
then A102: LIN o9,b19,b39 by AFF_1:def_1;
assume A103: a1 = a3 ; ::_thesis: a1,b2 // a2,b3
then a1,b1 // a1,b3 by A18, ANALMETR:59;
then a19,b19 // a19,b39 by ANALMETR:36;
hence a1,b2 // a2,b3 by A17, A103, A100, A102, AFF_1:14; ::_thesis: verum
end;
hence a1,b2 // a2,b3 by A21, A33; ::_thesis: verum
end;