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 AffinStruct(# the carrier of X, the CONGR of X #) ;

reconsider M9 = M, N9 = N as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;

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;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

reconsider M9 = M, N9 = N as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

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

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

not o,e1 // d1,e2

then consider d29 being Element of AffinStruct(# the carrier of X, the CONGR of 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 ;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

not o,e1 // d2,e2

then consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of 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 ;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

not o,e1 // d3,e2

then consider d49 being Element of AffinStruct(# the carrier of X, the CONGR of 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 ;

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

then A102: LIN d19,d39,b39 by A17, A32, A71, AFF_1:8;

then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of 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 ;

A107: d19 <> d39

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

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 AffinStruct(# the carrier of X, the CONGR of 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 ;

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 )

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

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN d19,d39,b39 by A140, ANALMETR:40;

then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of 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

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

then consider K9 being Subset of AffinStruct(# the carrier of X, the CONGR of 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 ;

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;

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;

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;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 AffinStruct(# the carrier of X, the CONGR of X #) ;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

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

A40:
not LIN b2,a3,b3
A37:
not LIN o9,b19,a29

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;proof

assume
b2 = b3
; :: thesis: contradiction
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;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

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

proof

A41:
a3 <> b3
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;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

proof

b29,b39 // b29,b19
by A8, A9, A10, A33, AFF_1:39, AFF_1:41;
assume
a3 = b3
; :: thesis: contradiction

then LIN b29,a39,b39 by AFF_1:7;

hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;then LIN b29,a39,b39 by AFF_1:7;

hence contradiction by A40, ANALMETR:40; :: thesis: verum

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

A47:
a3 <> b2
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;then LIN a39,a19,b29 by ANALMETR:40;

hence contradiction by A4, A6, A11, A30, A43, AFF_1:25; :: thesis: verum

proof

A48:
o,a3 _|_ o,b3
by A3, A6, A7, A10, A13, ANALMETR:56;
assume
a3 = b2
; :: thesis: contradiction

then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

not o,e1 // d1,e2

proof

then
not o9,e19 // d19,e29
by ANALMETR:36;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

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;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

then consider d29 being Element of AffinStruct(# the carrier of X, the CONGR of 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 ;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

not o,e1 // d2,e2

proof

then
not o9,e19 // d29,e29
by ANALMETR:36;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

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;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

then consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of 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 ;

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

not o,e1 // d3,e2

proof

then
not o9,e19 // d39,e29
by ANALMETR:36;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

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;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

then consider d49 being Element of AffinStruct(# the carrier of X, the CONGR of 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 ;

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

A91:
not LIN d1,d2,d3
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;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

proof

A100:
d2 <> d4
A92:
d2 <> d3

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

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;proof

A94:
d1 <> d2
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;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

proof

assume
LIN d1,d2,d3
; :: thesis: contradiction
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;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

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

LIN o9,a39,a19
by A45, ANALMETR:40;
assume
a1 = a3
; :: thesis: contradiction

then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

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

proof

LIN o9,b39,b39
by AFF_1:7;
A101:
d2 <> d3

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;proof

assume
d2 = d4
; :: thesis: contradiction
assume
d2 = d3
; :: thesis: contradiction

then LIN d19,d29,d39 by AFF_1:7;

hence contradiction by A91, ANALMETR:40; :: thesis: verum

end;then LIN d19,d29,d39 by AFF_1:7;

hence contradiction by A91, ANALMETR:40; :: thesis: verum

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

then A102: LIN d19,d39,b39 by A17, A32, A71, AFF_1:8;

then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of 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 ;

A107: d19 <> d39

proof

then
A9 = Line (d19,d39)
by A103, A104, A105, AFF_1:24;
assume
d19 = d39
; :: thesis: contradiction

then LIN d19,d29,d39 by AFF_1:7;

hence contradiction by A91, ANALMETR:40; :: thesis: verum

end;then LIN d19,d29,d39 by AFF_1:7;

hence contradiction by A91, ANALMETR:40; :: thesis: verum

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

A114:
o <> d4
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;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

proof

A117:
not LIN d1,d4,d3
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;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

proof

A130:
not d4 in A
A118:
d1 <> d3

then LIN d19,d49,d39 by ANALMETR:40;

then A125: LIN d19,d39,d49 by AFF_1:6;

A126: b29 <> b39

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;proof

assume
LIN d1,d4,d3
; :: thesis: contradiction
A119:
d1 <> d2

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

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;proof

assume
d1 = d3
; :: thesis: contradiction
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;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

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

LIN o9,a39,a19
by A45, ANALMETR:40;
assume
a1 = a3
; :: thesis: contradiction

then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

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

then LIN d19,d49,d39 by ANALMETR:40;

then A125: LIN d19,d39,d49 by AFF_1:6;

A126: b29 <> b39

proof

LIN o9,b29,b39
by A35, ANALMETR:40;
assume
b29 = b39
; :: thesis: contradiction

then LIN b29,a39,b39 by AFF_1:7;

hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;then LIN b29,a39,b39 by AFF_1:7;

hence contradiction by A40, ANALMETR:40; :: thesis: verum

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

proof

A131:
d2,d3 _|_ b3,a3
by A61, A62, A66, ANALMETR:62;
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;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

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 AffinStruct(# the carrier of X, the CONGR of 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 ;

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

LIN o9,b39,d39
by A70, ANALMETR:40;
A141:
b39 <> b29

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

A146: a39 <> a19

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;proof

LIN o9,b29,b39
by A35, ANALMETR:40;
assume
b39 = b29
; :: thesis: contradiction

then LIN b29,a39,b39 by AFF_1:7;

hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;then LIN b29,a39,b39 by AFF_1:7;

hence contradiction by A40, ANALMETR:40; :: thesis: verum

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

A146: a39 <> a19

proof

LIN o9,a39,a19
by A45, ANALMETR:40;
assume
a19 = a39
; :: thesis: contradiction

then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;then LIN a39,a19,b29 by AFF_1:7;

hence contradiction by A46, ANALMETR:40; :: thesis: verum

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

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

LIN o9,a39,d49
by A83, ANALMETR:40;
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;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

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 AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN d19,d39,b39 by A140, ANALMETR:40;

then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of 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

reconsider A = A9 as Subset of X ;
assume
d19 = d39
; :: thesis: contradiction

then LIN d19,d29,d39 by AFF_1:7;

hence contradiction by A91, ANALMETR:40; :: thesis: verum

end;then LIN d19,d29,d39 by AFF_1:7;

hence contradiction by A91, ANALMETR:40; :: thesis: verum

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

A164:
d1 <> d4
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;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

proof

A171:
not d4 in A
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;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

proof

LIN d29,d49,a19
by A140, ANALMETR:40;
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;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

then consider K9 being Subset of AffinStruct(# the carrier of X, the CONGR of 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 ;

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;

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;

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

now :: thesis: ( ( a1 = a2 or a2 = a3 or a1 = a3 ) implies a1,b2 // a2,b3 )

hence a1,b2 // a2,b3 by A179, A187, A183; :: thesis: verum

end;

hence
a1,b2 // a2,b3
by A22; :: thesis: verumA179: 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

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;then A180: LIN o9,b29,b39 by AFF_1:def 1;

assume A181: a1 = a2 ; :: thesis: a1,b2 // a2,b3

a1 <> b1

proof

then
a3,b2 // a3,b3
by A18, A19, A181, ANALMETR:60;
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 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

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

A183: now :: thesis: ( a1 = a3 implies a1,b2 // a2,b3 )

A184:
not LIN o9,a39,b19

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;proof

o9,b19 // o9,b39
by A7, A8, A10, A20, AFF_1:39, AFF_1:41;
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;then LIN o9,b19,a39 by AFF_1:6;

hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; :: thesis: verum

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

A187: now :: thesis: ( a2 = a3 implies a1,b2 // a2,b3 )

assume
( a1 = a2 or a2 = a3 or a1 = a3 )
; :: thesis: a1,b2 // a2,b3A188:
not LIN o9,a39,b19

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;proof

o9,b19 // o9,b29
by A7, A8, A9, A20, AFF_1:39, AFF_1:41;
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;then LIN o9,b19,a39 by AFF_1:6;

hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; :: thesis: verum

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

hence a1,b2 // a2,b3 by A179, A187, A183; :: thesis: verum