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

A21: M9 is being_line by A3, ANALMETR:43;

A22: N9 is being_line by A4, ANALMETR:43;

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

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 )

hence
a1,b2 // a2,b3
by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20; :: thesis: verumassume A23:
not M _|_ N
; :: thesis: a1,b2 // a2,b3

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

end;A25: a1 <> a2 and

A26: a2 <> a3 and

A27: a1 <> a3 ; :: thesis: a1,b2 // a2,b3

A28: ( b1 <> b2 & b2 <> b3 & b1 <> b3 )

proof

hence contradiction by A37, A33, A29; :: thesis: verum

end;

A29: now :: thesis: not b1 = b3

A30:
not LIN o9,b19,a19

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

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

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

A33: now :: thesis: not b2 = b3

A34:
not LIN o9,b19,a19

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

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

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

A37: now :: thesis: not b1 = b2

assume
( b1 = b2 or b2 = b3 or b1 = b3 )
; :: thesis: contradictionA38:
not LIN o9,b29,a29

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

assume
b1 = b2
; :: thesis: contradiction
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;then LIN o9,a29,b29 by AFF_1:6;

hence contradiction by A5, A7, A13, A16, A21, AFF_1:25; :: thesis: verum

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

hence contradiction by A37, A33, A29; :: thesis: verum

A40: now :: thesis: ( not a3,b3 _|_ o,b2 implies a1,b2 // a2,b3 )

A41:
not LIN b3,b1,a3

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

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

A48: a39,b39 // b29,e19 and

A49: b29 <> e19 by DIRAF:40;

reconsider x9 = x as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,x9 by AFF_1:7;

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

A53: for e1 being Element of X st e1 in A holds

LIN o,x,e1

e1 in A

then A56: A _|_ N by A46, A47, ANALMETR:def 14;

A57: not b2 in A

not b29,e19 // A9

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

A68: c39,a39 // a19,e19 and

A69: a19 <> e19 by DIRAF:40;

not a19,e19 // A9

A74: c19 in A9 and

A75: LIN a19,e19,c19 by A50, AFF_1:59;

reconsider c1 = c19 as Element of X ;

reconsider c3 = c39 as Element of X ;

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

A78: c39,a39 // a29,e19 and

A79: a29 <> e19 by DIRAF:40;

not a29,e19 // A9

A84: c29 in A9 and

A85: LIN a29,e19,c29 by A50, AFF_1:59;

reconsider c2 = c29 as Element of X ;

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 )

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

then A109: c1,a1 // c2,a2 by ANALMETR:59;

A110: not LIN c1,c2,b2

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;

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

o9,b29 // o9,b39
by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
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;then LIN b39,b19,a39 by ANALMETR:40;

hence contradiction by A10, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

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

o9,a39 // o9,a19
by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
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;then LIN b29,b19,a39 by ANALMETR:40;

hence contradiction by A10, A11, A14, A22, A28, AFF_1:25; :: thesis: verum

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

A48: a39,b39 // b29,e19 and

A49: b29 <> e19 by DIRAF:40;

reconsider x9 = x as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,x9 by AFF_1:7;

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

A53: for e1 being Element of X st e1 in A holds

LIN o,x,e1

proof

for e1 being Element of X st LIN o,x,e1 holds
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 AffinStruct(# the carrier of X, the CONGR of X #) ;

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;assume A54: e1 in A ; :: thesis: LIN o,x,e1

reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

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

e1 in A

proof

then
A = Line (o,x)
by A53, ANALMETR:def 11;
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 AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,e19 by A55, ANALMETR:40;

hence e1 in A by A46, A50, A51, A52, AFF_1:25; :: thesis: verum

end;assume A55: LIN o,x,e1 ; :: thesis: e1 in A

reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,e19 by A55, ANALMETR:40;

hence e1 in A by A46, A50, A51, A52, AFF_1:25; :: thesis: verum

then A56: A _|_ N by A46, A47, ANALMETR:def 14;

A57: not b2 in A

proof

assume A59:
not a3,b3 _|_ o,b2
; :: thesis: a1,b2 // a2,b3
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 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

not b29,e19 // A9

proof

then consider c39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
assume A60:
b29,e19 // A9
; :: thesis: contradiction

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

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

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

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

A68: c39,a39 // a19,e19 and

A69: a19 <> e19 by DIRAF:40;

not a19,e19 // A9

proof

then consider c19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A70:
c39 <> o9

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

assume A72:
a19,e19 // A9
; :: thesis: contradiction
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;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

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

A74: c19 in A9 and

A75: LIN a19,e19,c19 by A50, AFF_1:59;

reconsider c1 = c19 as Element of X ;

reconsider c3 = c39 as Element of X ;

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

A78: c39,a39 // a29,e19 and

A79: a29 <> e19 by DIRAF:40;

not a29,e19 // A9

proof

then consider c29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A80:
c39 <> o9

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

assume A82:
a29,e19 // A9
; :: thesis: contradiction
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;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

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

A84: c29 in A9 and

A85: LIN a29,e19,c29 by A50, AFF_1:59;

reconsider c2 = c29 as Element of X ;

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

hence contradiction by A89, A91; :: thesis: verum

end;

A95:
not c3 in N
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;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

A91: now :: thesis: ( not o = c2 & not o = c1 )

assume
( o = c3 or o = c2 or o = c1 )
; :: thesis: contradiction
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;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

hence contradiction by A89, A91; :: thesis: verum

proof

A97:
not LIN a3,a2,c3
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;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

proof

A99:
not LIN a3,a1,c3
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;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

proof

A101:
not LIN a1,a2,c1
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;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

proof

o9,a19 // o9,a29
by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
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;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

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

then
a1,c1 // a2,c2
by A77, A87, ANALMETR:60;
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;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

then A109: c1,a1 // c2,a2 by ANALMETR:59;

A110: not LIN c1,c2,b2

proof

o9,a39 // o9,a29
by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
A111:
c19 <> c29

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

assume
LIN c1,c2,b2
; :: thesis: contradiction
A112:
c3 <> a3

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

assume
c19 = c29
; :: thesis: contradiction
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 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

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

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

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;

hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A88, A103, A42, A105, A101, A110, A109, CONAFFM:def 1; :: thesis: verum

now :: thesis: ( a3,b3 _|_ o,b2 implies a1,b2 // a2,b3 )

hence
a1,b2 // a2,b3
by A40; :: thesis: verum
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 )

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

A128: a39,b29 // b39,e19 and

A129: b39 <> e19 by DIRAF:40;

reconsider x9 = x as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,x9 by AFF_1:7;

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

A133: for e1 being Element of X st e1 in A holds

LIN o,x,e1

e1 in A

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

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

A146: c39,a39 // a29,e19 and

A147: a29 <> e19 by DIRAF:40;

not a29,e19 // A9

A152: c29 in A9 and

A153: LIN a29,e19,c29 by A130, AFF_1:59;

reconsider c3 = c39 as Element of X ;

reconsider c2 = c29 as Element of X ;

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

A156: c39,a39 // a19,e19 and

A157: a19 <> e19 by DIRAF:40;

not a19,e19 // A9

A162: c19 in A9 and

A163: LIN a19,e19,c19 by A130, AFF_1:59;

reconsider c1 = c19 as Element of X ;

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 )

then LIN o9,c19,c29 by AFF_1:def 1;

then A187: LIN o,c1,c2 by ANALMETR:40;

a3 <> c3

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;

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

o9,a39 // o9,a29
by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
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;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

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

A128: a39,b29 // b39,e19 and

A129: b39 <> e19 by DIRAF:40;

reconsider x9 = x as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,x9 by AFF_1:7;

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

A133: for e1 being Element of X st e1 in A holds

LIN o,x,e1

proof

for e1 being Element of X st LIN o,x,e1 holds
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 AffinStruct(# the carrier of X, the CONGR of X #) ;

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;assume A134: e1 in A ; :: thesis: LIN o,x,e1

reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

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

e1 in A

proof

then
A = Line (o,x)
by A133, ANALMETR:def 11;
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 AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,e19 by A135, ANALMETR:40;

hence e1 in A by A126, A130, A131, A132, AFF_1:25; :: thesis: verum

end;assume A135: LIN o,x,e1 ; :: thesis: e1 in A

reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

LIN o9,x9,e19 by A135, ANALMETR:40;

hence e1 in A by A126, A130, A131, A132, AFF_1:25; :: thesis: verum

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

then consider c39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
assume A138:
b39,e19 // A9
; :: thesis: contradiction

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

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

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

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

A146: c39,a39 // a29,e19 and

A147: a29 <> e19 by DIRAF:40;

not a29,e19 // A9

proof

then consider c29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A148:
c39 <> o9

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

assume A150:
a29,e19 // A9
; :: thesis: contradiction
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;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

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

A152: c29 in A9 and

A153: LIN a29,e19,c29 by A130, AFF_1:59;

reconsider c3 = c39 as Element of X ;

reconsider c2 = c29 as Element of X ;

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

A156: c39,a39 // a19,e19 and

A157: a19 <> e19 by DIRAF:40;

not a19,e19 // A9

proof

then consider c19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A158:
c39 <> o9

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

assume A160:
a19,e19 // A9
; :: thesis: contradiction
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;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

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

A162: c19 in A9 and

A163: LIN a19,e19,c19 by A130, AFF_1:59;

reconsider c1 = c19 as Element of X ;

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

hence contradiction by A168, A170; :: thesis: verum

end;

A174:
not c3 in N
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;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

A170: now :: thesis: ( not o = c2 & not o = c1 )

assume
( o = c3 or o = c2 or o = c1 )
; :: thesis: contradiction
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;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

hence contradiction by A168, A170; :: thesis: verum

proof

A176:
not LIN a1,a2,c1
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;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

proof

A178:
( not LIN a3,a1,c3 & not LIN a3,a2,c3 )
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;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

proof

A180:
not b2 in A
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;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

proof

A182:
not LIN c1,c2,b2
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;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

proof

o9,c19 // o9,c29
by A130, A131, A152, A162, AFF_1:39, AFF_1:41;
A183:
c19 <> c29

then LIN c19,c29,b29 by ANALMETR:40;

hence contradiction by A130, A152, A162, A180, A183, AFF_1:25; :: thesis: verum

end;proof

assume
LIN c1,c2,b2
; :: thesis: contradiction
A184:
a3 <> c3

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

assume
c19 = c29
; :: thesis: contradiction
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 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

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

then LIN c19,c29,b29 by ANALMETR:40;

hence contradiction by A130, A152, A162, A180, A183, AFF_1:25; :: thesis: verum

then LIN o9,c19,c29 by AFF_1:def 1;

then A187: LIN o,c1,c2 by ANALMETR:40;

a3 <> c3

proof

then
a2,c2 // a1,c1
by A155, A165, ANALMETR:60;
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;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

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;

hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A167, A118, A120, A187, A176, A182, A189, CONAFFM:def 1; :: thesis: verum

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

A192:
not LIN o9,a39,b39

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

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

hence contradiction by A9, A12, A14, A18, A22, AFF_1:25; :: thesis: verum

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

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

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

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

a1 <> b1

proof

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

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

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

hence
a1,b2 // a2,b3
by A195, A191, A24; :: thesis: verum
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;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