let X be OrtAfPl; :: thesis: ( X is satisfying_3H implies X is satisfying_OPAP )

assume A1: X is satisfying_3H ; :: thesis: X is satisfying_OPAP

let o be Element of X; :: according to CONMETR:def 1 :: thesis: for a1, a2, a3, b1, b2, b3 being Element of X

for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds

a1,b2 // a2,b3

let a1, a2, a3, b1, b2, b3 be Element of X; :: thesis: for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds

a1,b2 // a2,b3

let M, N be Subset of X; :: thesis: ( o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )

assume that

A2: o in M and

A3: a1 in M and

A4: a2 in M and

A5: a3 in M and

A6: o in N and

A7: b1 in N and

A8: b2 in N and

A9: b3 in N and

A10: not b2 in M and

A11: not a3 in N and

A12: M _|_ N and

A13: o <> a1 and

A14: o <> a2 and

o <> a3 and

A15: o <> b1 and

o <> b2 and

A16: o <> b3 and

A17: a3,b2 // a2,b1 and

A18: a3,b3 // a1,b1 ; :: thesis: a1,b2 // a2,b3

reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of 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 A12, ANALMETR:44;

then A19: N9 is being_line by ANALMETR:43;

M is being_line by A12, ANALMETR:44;

then A20: M9 is being_line by ANALMETR:43;

( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )

assume A1: X is satisfying_3H ; :: thesis: X is satisfying_OPAP

let o be Element of X; :: according to CONMETR:def 1 :: thesis: for a1, a2, a3, b1, b2, b3 being Element of X

for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds

a1,b2 // a2,b3

let a1, a2, a3, b1, b2, b3 be Element of X; :: thesis: for M, N being Subset of X st o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 holds

a1,b2 // a2,b3

let M, N be Subset of X; :: thesis: ( o in M & a1 in M & a2 in M & a3 in M & o in N & b1 in N & b2 in N & b3 in N & not b2 in M & not a3 in N & M _|_ N & o <> a1 & o <> a2 & o <> a3 & o <> b1 & o <> b2 & o <> b3 & a3,b2 // a2,b1 & a3,b3 // a1,b1 implies a1,b2 // a2,b3 )

assume that

A2: o in M and

A3: a1 in M and

A4: a2 in M and

A5: a3 in M and

A6: o in N and

A7: b1 in N and

A8: b2 in N and

A9: b3 in N and

A10: not b2 in M and

A11: not a3 in N and

A12: M _|_ N and

A13: o <> a1 and

A14: o <> a2 and

o <> a3 and

A15: o <> b1 and

o <> b2 and

A16: o <> b3 and

A17: a3,b2 // a2,b1 and

A18: a3,b3 // a1,b1 ; :: thesis: a1,b2 // a2,b3

reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, b19 = b1, b29 = b2, b39 = b3 as Element of 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 A12, ANALMETR:44;

then A19: N9 is being_line by ANALMETR:43;

M is being_line by A12, ANALMETR:44;

then A20: M9 is being_line by ANALMETR:43;

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

A27:
for a, b, c being Element of X st LIN a,b,c holds A22:
not LIN o9,b19,a19

o9,a19 // o9,a29 by A2, A3, A4, A20, AFF_1:39, AFF_1:41;

then A25: LIN o9,a19,a29 by AFF_1:def 1;

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

then b1,a1 // a3,b2 by A18, ANALMETR:59;

then b1,a1 // b1,a2 by A5, A10, A24, ANALMETR:60;

then b19,a19 // b19,a29 by ANALMETR:36;

then a19 = a29 by A22, A25, AFF_1:14;

then a19,b29 // a29,b39 by A26, AFF_1:2;

hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum

end;proof

A24:
b1,a2 // a3,b2
by A17, ANALMETR:59;
o9,a19 // o9,a39
by A2, A3, A5, A20, AFF_1:39, AFF_1:41;

then A23: LIN o9,a19,a39 by AFF_1:def 1;

assume LIN o9,b19,a19 ; :: thesis: contradiction

then a19 in N9 by A6, A7, A15, A19, AFF_1:25;

hence contradiction by A6, A11, A13, A19, A23, AFF_1:25; :: thesis: verum

end;then A23: LIN o9,a19,a39 by AFF_1:def 1;

assume LIN o9,b19,a19 ; :: thesis: contradiction

then a19 in N9 by A6, A7, A15, A19, AFF_1:25;

hence contradiction by A6, A11, A13, A19, A23, AFF_1:25; :: thesis: verum

o9,a19 // o9,a29 by A2, A3, A4, A20, AFF_1:39, AFF_1:41;

then A25: LIN o9,a19,a29 by AFF_1:def 1;

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

then b1,a1 // a3,b2 by A18, ANALMETR:59;

then b1,a1 // b1,a2 by A5, A10, A24, ANALMETR:60;

then b19,a19 // b19,a29 by ANALMETR:36;

then a19 = a29 by A22, A25, AFF_1:14;

then a19,b29 // a29,b39 by A26, AFF_1:2;

hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum

( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )

proof

let a, b, c be Element of X; :: thesis: ( LIN a,b,c implies ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) )

reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

assume LIN a,b,c ; :: thesis: ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )

then A28: LIN a9,b9,c9 by ANALMETR:40;

then A29: LIN b9,a9,c9 by AFF_1:6;

A30: LIN c9,a9,b9 by A28, AFF_1:6;

A31: LIN b9,c9,a9 by A28, AFF_1:6;

A32: LIN c9,b9,a9 by A28, AFF_1:6;

LIN a9,c9,b9 by A28, AFF_1:6;

hence ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) by A29, A31, A30, A32, ANALMETR:40; :: thesis: verum

end;reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

assume LIN a,b,c ; :: thesis: ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a )

then A28: LIN a9,b9,c9 by ANALMETR:40;

then A29: LIN b9,a9,c9 by AFF_1:6;

A30: LIN c9,a9,b9 by A28, AFF_1:6;

A31: LIN b9,c9,a9 by A28, AFF_1:6;

A32: LIN c9,b9,a9 by A28, AFF_1:6;

LIN a9,c9,b9 by A28, AFF_1:6;

hence ( LIN a,c,b & LIN b,a,c & LIN b,c,a & LIN c,a,b & LIN c,b,a ) by A29, A31, A30, A32, ANALMETR:40; :: thesis: verum

A33: now :: thesis: ( a1 <> a3 & b2 <> b3 implies a1,b2 // a2,b3 )

o9,a39 // o9,a19
by A2, A3, A5, A20, AFF_1:39, AFF_1:41;

then LIN o9,a39,a19 by AFF_1:def 1;

then A34: LIN o,a3,a1 by ANALMETR:40;

a39,a19 // a39,a29 by A3, A4, A5, A20, AFF_1:39, AFF_1:41;

then LIN a39,a19,a29 by AFF_1:def 1;

then A35: LIN a3,a1,a2 by ANALMETR:40;

o9,b29 // o9,b39 by A6, A8, A9, A19, AFF_1:39, AFF_1:41;

then LIN o9,b29,b39 by AFF_1:def 1;

then A36: LIN o,b2,b3 by ANALMETR:40;

assume that

A37: a1 <> a3 and

A38: b2 <> b3 ; :: thesis: a1,b2 // a2,b3

A39: ( not LIN a3,a1,b2 & not LIN b2,a3,b3 )

then LIN b29,b39,b19 by AFF_1:def 1;

then A40: LIN b2,b3,b1 by ANALMETR:40;

end;then LIN o9,a39,a19 by AFF_1:def 1;

then A34: LIN o,a3,a1 by ANALMETR:40;

a39,a19 // a39,a29 by A3, A4, A5, A20, AFF_1:39, AFF_1:41;

then LIN a39,a19,a29 by AFF_1:def 1;

then A35: LIN a3,a1,a2 by ANALMETR:40;

o9,b29 // o9,b39 by A6, A8, A9, A19, AFF_1:39, AFF_1:41;

then LIN o9,b29,b39 by AFF_1:def 1;

then A36: LIN o,b2,b3 by ANALMETR:40;

assume that

A37: a1 <> a3 and

A38: b2 <> b3 ; :: thesis: a1,b2 // a2,b3

A39: ( not LIN a3,a1,b2 & not LIN b2,a3,b3 )

proof

b29,b39 // b29,b19
by A7, A8, A9, A19, AFF_1:39, AFF_1:41;
assume
( LIN a3,a1,b2 or LIN b2,a3,b3 )
; :: thesis: contradiction

then ( LIN a39,a19,b29 or LIN b29,a39,b39 ) by ANALMETR:40;

then ( LIN a39,a19,b29 or LIN b29,b39,a39 ) by AFF_1:6;

hence contradiction by A3, A5, A8, A9, A10, A11, A20, A19, A37, A38, AFF_1:25; :: thesis: verum

end;then ( LIN a39,a19,b29 or LIN b29,a39,b39 ) by ANALMETR:40;

then ( LIN a39,a19,b29 or LIN b29,b39,a39 ) by AFF_1:6;

hence contradiction by A3, A5, A8, A9, A10, A11, A20, A19, A37, A38, AFF_1:25; :: thesis: verum

then LIN b29,b39,b19 by AFF_1:def 1;

then A40: LIN b2,b3,b1 by ANALMETR:40;

A41: now :: thesis: ( b2 <> b1 implies a1,b2 // a2,b3 )

assume A42:
b2 <> b1
; :: thesis: a1,b2 // a2,b3

not LIN a2,a3,b3

A50: c1,a2 _|_ a3,b3 and

A51: c1,a3 _|_ a2,b3 and

A52: c1,b3 _|_ a2,a3 by A1, CONAFFM:def 3;

reconsider c19 = c1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

end;not LIN a2,a3,b3

proof

then consider c1 being Element of X such that
A43:
a3 <> a2

then A45: a3,a1 // a3,o by ANALMETR:def 10;

A46: a3 <> a1

then LIN a3,a2,b3 by A27;

then A47: a3,a2 // a3,b3 by ANALMETR:def 10;

LIN a3,a2,a1 by A27, A35;

then a3,a2 // a3,a1 by ANALMETR:def 10;

then a3,a1 // a3,b3 by A47, A43, ANALMETR:60;

then a3,o // a3,b3 by A46, A45, ANALMETR:60;

then a39,o9 // a39,b39 by ANALMETR:36;

then A48: a39,b39 // a39,o9 by AFF_1:4;

LIN b2,b3,o by A27, A36;

then A49: LIN b29,b39,o9 by ANALMETR:40;

not LIN b29,a39,b39 by A39, ANALMETR:40;

hence contradiction by A16, A48, A49, AFF_1:14; :: thesis: verum

end;proof

LIN a3,a1,o
by A27, A34;
assume
a3 = a2
; :: thesis: contradiction

then LIN a3,b2,b1 by A17, ANALMETR:def 10;

then LIN b2,b1,a3 by A27;

then A44: b2,b1 // b2,a3 by ANALMETR:def 10;

LIN b2,b1,b3 by A27, A40;

then b2,b1 // b2,b3 by ANALMETR:def 10;

then b2,a3 // b2,b3 by A42, A44, ANALMETR:60;

hence contradiction by A39, ANALMETR:def 10; :: thesis: verum

end;then LIN a3,b2,b1 by A17, ANALMETR:def 10;

then LIN b2,b1,a3 by A27;

then A44: b2,b1 // b2,a3 by ANALMETR:def 10;

LIN b2,b1,b3 by A27, A40;

then b2,b1 // b2,b3 by ANALMETR:def 10;

then b2,a3 // b2,b3 by A42, A44, ANALMETR:60;

hence contradiction by A39, ANALMETR:def 10; :: thesis: verum

then A45: a3,a1 // a3,o by ANALMETR:def 10;

A46: a3 <> a1

proof

assume
LIN a2,a3,b3
; :: thesis: contradiction
assume
a3 = a1
; :: thesis: contradiction

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

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

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

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

then LIN a3,a2,b3 by A27;

then A47: a3,a2 // a3,b3 by ANALMETR:def 10;

LIN a3,a2,a1 by A27, A35;

then a3,a2 // a3,a1 by ANALMETR:def 10;

then a3,a1 // a3,b3 by A47, A43, ANALMETR:60;

then a3,o // a3,b3 by A46, A45, ANALMETR:60;

then a39,o9 // a39,b39 by ANALMETR:36;

then A48: a39,b39 // a39,o9 by AFF_1:4;

LIN b2,b3,o by A27, A36;

then A49: LIN b29,b39,o9 by ANALMETR:40;

not LIN b29,a39,b39 by A39, ANALMETR:40;

hence contradiction by A16, A48, A49, AFF_1:14; :: thesis: verum

A50: c1,a2 _|_ a3,b3 and

A51: c1,a3 _|_ a2,b3 and

A52: c1,b3 _|_ a2,a3 by A1, CONAFFM:def 3;

reconsider c19 = c1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

A53: now :: thesis: ( a2 <> a1 implies a1,b2 // a2,b3 )

A54:
a2 <> a3

then b2,b3 // c1,b3 by A52, A54, ANALMETR:63;

then b3,b2 // b3,c1 by ANALMETR:59;

then LIN b3,b2,c1 by ANALMETR:def 10;

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

then A57: c1 in N by A8, A9, A19, A38, AFF_1:25;

A58: not LIN o9,a29,c19

A65: a1 <> b1

A69: c2,a2 _|_ a1,b1 and

A70: c2,a1 _|_ a2,b1 and

A71: c2,b1 _|_ a2,a1 by A1, CONAFFM:def 3;

reconsider c29 = c2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

a1,b1 _|_ c1,a2 by A9, A11, A18, A50, ANALMETR:62;

then c2,a2 // c1,a2 by A69, A62, ANALMETR:63;

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

then A72: a29,c19 // a29,c29 by ANALMETR:36;

a2,a1 _|_ b1,b2 by A3, A4, A7, A8, A12, ANALMETR:56;

then b1,b2 // c2,b1 by A64, A71, ANALMETR:63;

then b1,b2 // b1,c2 by ANALMETR:59;

then LIN b1,b2,c2 by ANALMETR:def 10;

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

then A73: c29 in N9 by A7, A8, A19, A42, AFF_1:25;

A74: not LIN o9,a19,c29

A80: c3,a3 _|_ a1,b2 and

A81: c3,a1 _|_ a3,b2 and

A82: c3,b2 _|_ a3,a1 by A1, CONAFFM:def 3;

reconsider c39 = c3 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

a2 <> b1

then c2,a1 // c3,a1 by A5, A10, A81, ANALMETR:63;

then a1,c2 // a1,c3 by ANALMETR:59;

then A84: a19,c29 // a19,c39 by ANALMETR:36;

a2,a1 _|_ b2,b1 by A3, A4, A7, A8, A12, ANALMETR:56;

then b2,b1 // c2,b1 by A64, A71, ANALMETR:63;

then b1,b2 // b1,c2 by ANALMETR:59;

then LIN b1,b2,c2 by ANALMETR:def 10;

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

then c2 in N by A7, A8, A19, A42, AFF_1:25;

then o9,c19 // o9,c29 by A6, A19, A57, AFF_1:39, AFF_1:41;

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

then A85: c1 = c2 by A58, A72, AFF_1:14;

A86: c1 <> a3

then c3,b2 // b2,b3 by A37, A82, ANALMETR:63;

then b2,b3 // b2,c3 by ANALMETR:59;

then LIN b2,b3,c3 by ANALMETR:def 10;

then LIN b29,b39,c39 by ANALMETR:40;

then c39 in N9 by A8, A9, A19, A38, AFF_1:25;

then o9,c29 // o9,c39 by A6, A19, A73, AFF_1:39, AFF_1:41;

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

then c2 = c3 by A74, A84, AFF_1:14;

hence a1,b2 // a2,b3 by A51, A85, A80, A86, ANALMETR:63; :: thesis: verum

end;proof

a2,a3 _|_ b2,b3
by A4, A5, A8, A9, A12, ANALMETR:56;
A55:
not LIN o9,a39,b19

then a39,b29 // a39,b19 by A17, ANALMETR:36;

then A56: a39,b19 // a39,b29 by AFF_1:4;

o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then LIN o9,b19,b29 by AFF_1:def 1;

hence contradiction by A42, A55, A56, AFF_1:14; :: thesis: verum

end;proof

assume
a2 = a3
; :: thesis: contradiction
assume
LIN o9,a39,b19
; :: thesis: contradiction

then LIN o9,b19,a39 by AFF_1:6;

hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; :: thesis: verum

end;then LIN o9,b19,a39 by AFF_1:6;

hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; :: thesis: verum

then a39,b29 // a39,b19 by A17, ANALMETR:36;

then A56: a39,b19 // a39,b29 by AFF_1:4;

o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then LIN o9,b19,b29 by AFF_1:def 1;

hence contradiction by A42, A55, A56, AFF_1:14; :: thesis: verum

then b2,b3 // c1,b3 by A52, A54, ANALMETR:63;

then b3,b2 // b3,c1 by ANALMETR:59;

then LIN b3,b2,c1 by ANALMETR:def 10;

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

then A57: c1 in N by A8, A9, A19, A38, AFF_1:25;

A58: not LIN o9,a29,c19

proof

A62:
a1 <> b1
A59:
o9 <> c19

then A61: LIN o9,a29,a39 by AFF_1:def 1;

assume LIN o9,a29,c19 ; :: thesis: contradiction

then LIN o9,c19,a29 by AFF_1:6;

then a29 in N9 by A6, A19, A57, A59, AFF_1:25;

hence contradiction by A6, A11, A14, A19, A61, AFF_1:25; :: thesis: verum

end;proof

o9,a29 // o9,a39
by A2, A4, A5, A20, AFF_1:39, AFF_1:41;
assume A60:
o9 = c19
; :: thesis: contradiction

o,a2 _|_ b3,b2 by A2, A4, A8, A9, A12, ANALMETR:56;

then b3,b2 // a3,b3 by A14, A50, A60, ANALMETR:63;

then b3,b2 // b3,a3 by ANALMETR:59;

then LIN b3,b2,a3 by ANALMETR:def 10;

then LIN b39,b29,a39 by ANALMETR:40;

hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum

end;o,a2 _|_ b3,b2 by A2, A4, A8, A9, A12, ANALMETR:56;

then b3,b2 // a3,b3 by A14, A50, A60, ANALMETR:63;

then b3,b2 // b3,a3 by ANALMETR:59;

then LIN b3,b2,a3 by ANALMETR:def 10;

then LIN b39,b29,a39 by ANALMETR:40;

hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum

then A61: LIN o9,a29,a39 by AFF_1:def 1;

assume LIN o9,a29,c19 ; :: thesis: contradiction

then LIN o9,c19,a29 by AFF_1:6;

then a29 in N9 by A6, A19, A57, A59, AFF_1:25;

hence contradiction by A6, A11, A14, A19, A61, AFF_1:25; :: thesis: verum

proof

assume A64:
a2 <> a1
; :: thesis: a1,b2 // a2,b3
o9,b19 // o9,b29
by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then A63: LIN o9,b19,b29 by AFF_1:def 1;

assume a1 = b1 ; :: thesis: contradiction

hence contradiction by A2, A3, A10, A13, A20, A63, AFF_1:25; :: thesis: verum

end;then A63: LIN o9,b19,b29 by AFF_1:def 1;

assume a1 = b1 ; :: thesis: contradiction

hence contradiction by A2, A3, A10, A13, A20, A63, AFF_1:25; :: thesis: verum

A65: a1 <> b1

proof

not LIN a2,a1,b1
LIN a1,a2,a3
by A27, A35;

then a1,a2 // a1,a3 by ANALMETR:def 10;

then A66: a2,a1 // a3,a1 by ANALMETR:59;

assume a1 = b1 ; :: thesis: contradiction

then a3,a1 // a3,b2 by A17, A64, A66, ANALMETR:60;

hence contradiction by A39, ANALMETR:def 10; :: thesis: verum

end;then a1,a2 // a1,a3 by ANALMETR:def 10;

then A66: a2,a1 // a3,a1 by ANALMETR:59;

assume a1 = b1 ; :: thesis: contradiction

then a3,a1 // a3,b2 by A17, A64, A66, ANALMETR:60;

hence contradiction by A39, ANALMETR:def 10; :: thesis: verum

proof

then consider c2 being Element of X such that
assume
LIN a2,a1,b1
; :: thesis: contradiction

then LIN b1,a1,a2 by A27;

then b1,a1 // b1,a2 by ANALMETR:def 10;

then a1,b1 // a2,b1 by ANALMETR:59;

then A67: a2,b1 // a3,b3 by A18, A65, ANALMETR:60;

a2 <> b1

then LIN a3,b3,b2 by ANALMETR:def 10;

hence contradiction by A27, A39; :: thesis: verum

end;then LIN b1,a1,a2 by A27;

then b1,a1 // b1,a2 by ANALMETR:def 10;

then a1,b1 // a2,b1 by ANALMETR:59;

then A67: a2,b1 // a3,b3 by A18, A65, ANALMETR:60;

a2 <> b1

proof

then
a3,b3 // a3,b2
by A17, A67, ANALMETR:60;
o9,b19 // o9,b29
by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then A68: LIN o9,b19,b29 by AFF_1:def 1;

assume a2 = b1 ; :: thesis: contradiction

hence contradiction by A2, A4, A10, A14, A20, A68, AFF_1:25; :: thesis: verum

end;then A68: LIN o9,b19,b29 by AFF_1:def 1;

assume a2 = b1 ; :: thesis: contradiction

hence contradiction by A2, A4, A10, A14, A20, A68, AFF_1:25; :: thesis: verum

then LIN a3,b3,b2 by ANALMETR:def 10;

hence contradiction by A27, A39; :: thesis: verum

A69: c2,a2 _|_ a1,b1 and

A70: c2,a1 _|_ a2,b1 and

A71: c2,b1 _|_ a2,a1 by A1, CONAFFM:def 3;

reconsider c29 = c2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

a1,b1 _|_ c1,a2 by A9, A11, A18, A50, ANALMETR:62;

then c2,a2 // c1,a2 by A69, A62, ANALMETR:63;

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

then A72: a29,c19 // a29,c29 by ANALMETR:36;

a2,a1 _|_ b1,b2 by A3, A4, A7, A8, A12, ANALMETR:56;

then b1,b2 // c2,b1 by A64, A71, ANALMETR:63;

then b1,b2 // b1,c2 by ANALMETR:59;

then LIN b1,b2,c2 by ANALMETR:def 10;

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

then A73: c29 in N9 by A7, A8, A19, A42, AFF_1:25;

A74: not LIN o9,a19,c29

proof

not LIN a3,a1,b2
A75:
o9 <> c29

then A79: LIN o9,a19,a39 by AFF_1:def 1;

assume LIN o9,a19,c29 ; :: thesis: contradiction

then LIN o9,c29,a19 by AFF_1:6;

then a19 in N9 by A6, A19, A73, A75, AFF_1:25;

hence contradiction by A6, A11, A13, A19, A79, AFF_1:25; :: thesis: verum

end;proof

o9,a19 // o9,a39
by A2, A3, A5, A20, AFF_1:39, AFF_1:41;
A76:
a2 <> b1

then A78: o,a1 _|_ a3,b2 by A17, A70, A76, ANALMETR:62;

o,a1 _|_ b3,b2 by A2, A3, A8, A9, A12, ANALMETR:56;

then b3,b2 // a3,b2 by A13, A78, ANALMETR:63;

then b2,b3 // b2,a3 by ANALMETR:59;

then LIN b2,b3,a3 by ANALMETR:def 10;

then LIN b29,b39,a39 by ANALMETR:40;

hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum

end;proof

assume
o9 = c29
; :: thesis: contradiction
o9,b19 // o9,b29
by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then A77: LIN o9,b19,b29 by AFF_1:def 1;

assume a2 = b1 ; :: thesis: contradiction

hence contradiction by A2, A4, A10, A14, A20, A77, AFF_1:25; :: thesis: verum

end;then A77: LIN o9,b19,b29 by AFF_1:def 1;

assume a2 = b1 ; :: thesis: contradiction

hence contradiction by A2, A4, A10, A14, A20, A77, AFF_1:25; :: thesis: verum

then A78: o,a1 _|_ a3,b2 by A17, A70, A76, ANALMETR:62;

o,a1 _|_ b3,b2 by A2, A3, A8, A9, A12, ANALMETR:56;

then b3,b2 // a3,b2 by A13, A78, ANALMETR:63;

then b2,b3 // b2,a3 by ANALMETR:59;

then LIN b2,b3,a3 by ANALMETR:def 10;

then LIN b29,b39,a39 by ANALMETR:40;

hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum

then A79: LIN o9,a19,a39 by AFF_1:def 1;

assume LIN o9,a19,c29 ; :: thesis: contradiction

then LIN o9,c29,a19 by AFF_1:6;

then a19 in N9 by A6, A19, A73, A75, AFF_1:25;

hence contradiction by A6, A11, A13, A19, A79, AFF_1:25; :: thesis: verum

proof

then consider c3 being Element of X such that
assume
LIN a3,a1,b2
; :: thesis: contradiction

then LIN a39,a19,b29 by ANALMETR:40;

hence contradiction by A3, A5, A10, A20, A37, AFF_1:25; :: thesis: verum

end;then LIN a39,a19,b29 by ANALMETR:40;

hence contradiction by A3, A5, A10, A20, A37, AFF_1:25; :: thesis: verum

A80: c3,a3 _|_ a1,b2 and

A81: c3,a1 _|_ a3,b2 and

A82: c3,b2 _|_ a3,a1 by A1, CONAFFM:def 3;

reconsider c39 = c3 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

a2 <> b1

proof

then
a3,b2 _|_ c2,a1
by A17, A70, ANALMETR:62;
o9,b19 // o9,b29
by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then A83: LIN o9,b19,b29 by AFF_1:def 1;

assume a2 = b1 ; :: thesis: contradiction

hence contradiction by A2, A4, A10, A14, A20, A83, AFF_1:25; :: thesis: verum

end;then A83: LIN o9,b19,b29 by AFF_1:def 1;

assume a2 = b1 ; :: thesis: contradiction

hence contradiction by A2, A4, A10, A14, A20, A83, AFF_1:25; :: thesis: verum

then c2,a1 // c3,a1 by A5, A10, A81, ANALMETR:63;

then a1,c2 // a1,c3 by ANALMETR:59;

then A84: a19,c29 // a19,c39 by ANALMETR:36;

a2,a1 _|_ b2,b1 by A3, A4, A7, A8, A12, ANALMETR:56;

then b2,b1 // c2,b1 by A64, A71, ANALMETR:63;

then b1,b2 // b1,c2 by ANALMETR:59;

then LIN b1,b2,c2 by ANALMETR:def 10;

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

then c2 in N by A7, A8, A19, A42, AFF_1:25;

then o9,c19 // o9,c29 by A6, A19, A57, AFF_1:39, AFF_1:41;

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

then A85: c1 = c2 by A58, A72, AFF_1:14;

A86: c1 <> a3

proof

a3,a1 _|_ b2,b3
by A3, A5, A8, A9, A12, ANALMETR:56;
A87:
a2 <> a3

a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:56;

then a3,b3 // b2,b3 by A52, A90, A87, ANALMETR:63;

then b3,b2 // b3,a3 by ANALMETR:59;

then LIN b3,b2,a3 by ANALMETR:def 10;

then LIN b39,b29,a39 by ANALMETR:40;

hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum

end;proof

assume A90:
c1 = a3
; :: thesis: contradiction
A88:
not LIN o9,a39,b19

then a39,b29 // a39,b19 by A17, ANALMETR:36;

then A89: a39,b19 // a39,b29 by AFF_1:4;

o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then LIN o9,b19,b29 by AFF_1:def 1;

hence contradiction by A42, A88, A89, AFF_1:14; :: thesis: verum

end;proof

assume
a2 = a3
; :: thesis: contradiction
assume
LIN o9,a39,b19
; :: thesis: contradiction

then LIN o9,b19,a39 by AFF_1:6;

hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; :: thesis: verum

end;then LIN o9,b19,a39 by AFF_1:6;

hence contradiction by A6, A7, A11, A15, A19, AFF_1:25; :: thesis: verum

then a39,b29 // a39,b19 by A17, ANALMETR:36;

then A89: a39,b19 // a39,b29 by AFF_1:4;

o9,b19 // o9,b29 by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then LIN o9,b19,b29 by AFF_1:def 1;

hence contradiction by A42, A88, A89, AFF_1:14; :: thesis: verum

a2,a3 _|_ b2,b3 by A4, A5, A8, A9, A12, ANALMETR:56;

then a3,b3 // b2,b3 by A52, A90, A87, ANALMETR:63;

then b3,b2 // b3,a3 by ANALMETR:59;

then LIN b3,b2,a3 by ANALMETR:def 10;

then LIN b39,b29,a39 by ANALMETR:40;

hence contradiction by A8, A9, A11, A19, A38, AFF_1:25; :: thesis: verum

then c3,b2 // b2,b3 by A37, A82, ANALMETR:63;

then b2,b3 // b2,c3 by ANALMETR:59;

then LIN b2,b3,c3 by ANALMETR:def 10;

then LIN b29,b39,c39 by ANALMETR:40;

then c39 in N9 by A8, A9, A19, A38, AFF_1:25;

then o9,c29 // o9,c39 by A6, A19, A73, AFF_1:39, AFF_1:41;

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

then c2 = c3 by A74, A84, AFF_1:14;

hence a1,b2 // a2,b3 by A51, A85, A80, A86, ANALMETR:63; :: thesis: verum

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

hence
a1,b2 // a2,b3
by A53; :: thesis: verum
o9,b29 // o9,b39
by A6, A8, A9, A19, AFF_1:39, AFF_1:41;

then A91: LIN o9,b29,b39 by AFF_1:def 1;

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

a1 <> b1

then a39,b29 // a39,b39 by ANALMETR:36;

then b29 = b39 by A2, A5, A6, A10, A11, A20, A91, AFF_1:14, AFF_1:25;

then a19,b29 // a29,b39 by A92, AFF_1:2;

hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum

end;then A91: LIN o9,b29,b39 by AFF_1:def 1;

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

a1 <> b1

proof

then
a3,b2 // a3,b3
by A17, A18, A92, ANALMETR:60;
o9,b19 // o9,b29
by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then A93: LIN o9,b19,b29 by AFF_1:def 1;

assume a1 = b1 ; :: thesis: contradiction

hence contradiction by A2, A3, A10, A13, A20, A93, AFF_1:25; :: thesis: verum

end;then A93: LIN o9,b19,b29 by AFF_1:def 1;

assume a1 = b1 ; :: thesis: contradiction

hence contradiction by A2, A3, A10, A13, A20, A93, AFF_1:25; :: thesis: verum

then a39,b29 // a39,b39 by ANALMETR:36;

then b29 = b39 by A2, A5, A6, A10, A11, A20, A91, AFF_1:14, AFF_1:25;

then a19,b29 // a29,b39 by A92, AFF_1:2;

hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum

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

hence
a1,b2 // a2,b3
by A41; :: thesis: verumA94:
not LIN o9,b29,a39

then A96: a3,a1 // a3,o by ANALMETR:def 10;

A97: a3 <> a1

then a3,o // a3,a2 by A96, A97, ANALMETR:60;

then LIN a3,o,a2 by ANALMETR:def 10;

then LIN o,a3,a2 by A27;

then A98: LIN o9,a39,a29 by ANALMETR:40;

assume A99: b2 = b1 ; :: thesis: a1,b2 // a2,b3

then b2,a3 // b2,a2 by A17, ANALMETR:59;

then b29,a39 // b29,a29 by ANALMETR:36;

then a39 = a29 by A98, A94, AFF_1:14;

hence a1,b2 // a2,b3 by A18, A99, ANALMETR:59; :: thesis: verum

end;proof

LIN a3,a1,o
by A27, A34;
assume
LIN o9,b29,a39
; :: thesis: contradiction

then LIN o,b2,a3 by ANALMETR:40;

then LIN b2,o,a3 by A27;

then A95: b2,o // b2,a3 by ANALMETR:def 10;

LIN b2,o,b3 by A27, A36;

then b2,o // b2,b3 by ANALMETR:def 10;

then b2,a3 // b2,b3 by A2, A10, A95, ANALMETR:60;

hence contradiction by A39, ANALMETR:def 10; :: thesis: verum

end;then LIN o,b2,a3 by ANALMETR:40;

then LIN b2,o,a3 by A27;

then A95: b2,o // b2,a3 by ANALMETR:def 10;

LIN b2,o,b3 by A27, A36;

then b2,o // b2,b3 by ANALMETR:def 10;

then b2,a3 // b2,b3 by A2, A10, A95, ANALMETR:60;

hence contradiction by A39, ANALMETR:def 10; :: thesis: verum

then A96: a3,a1 // a3,o by ANALMETR:def 10;

A97: a3 <> a1

proof

a3,a1 // a3,a2
by A35, ANALMETR:def 10;
assume
a3 = a1
; :: thesis: contradiction

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

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

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

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

then a3,o // a3,a2 by A96, A97, ANALMETR:60;

then LIN a3,o,a2 by ANALMETR:def 10;

then LIN o,a3,a2 by A27;

then A98: LIN o9,a39,a29 by ANALMETR:40;

assume A99: b2 = b1 ; :: thesis: a1,b2 // a2,b3

then b2,a3 // b2,a2 by A17, ANALMETR:59;

then b29,a39 // b29,a29 by ANALMETR:36;

then a39 = a29 by A98, A94, AFF_1:14;

hence a1,b2 // a2,b3 by A18, A99, ANALMETR:59; :: thesis: verum

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

hence
a1,b2 // a2,b3
by A21, A33; :: thesis: verumA100:
not LIN o9,a19,b19

then A102: LIN o9,b19,b39 by AFF_1:def 1;

assume A103: a1 = a3 ; :: thesis: a1,b2 // a2,b3

then a1,b1 // a1,b3 by A18, ANALMETR:59;

then a19,b19 // a19,b39 by ANALMETR:36;

hence a1,b2 // a2,b3 by A17, A103, A100, A102, AFF_1:14; :: thesis: verum

end;proof

o9,b19 // o9,b39
by A6, A7, A9, A19, AFF_1:39, AFF_1:41;
o9,b19 // o9,b29
by A6, A7, A8, A19, AFF_1:39, AFF_1:41;

then A101: LIN o9,b19,b29 by AFF_1:def 1;

assume LIN o9,a19,b19 ; :: thesis: contradiction

then b19 in M9 by A2, A3, A13, A20, AFF_1:25;

hence contradiction by A2, A10, A15, A20, A101, AFF_1:25; :: thesis: verum

end;then A101: LIN o9,b19,b29 by AFF_1:def 1;

assume LIN o9,a19,b19 ; :: thesis: contradiction

then b19 in M9 by A2, A3, A13, A20, AFF_1:25;

hence contradiction by A2, A10, A15, A20, A101, AFF_1:25; :: thesis: verum

then A102: LIN o9,b19,b39 by AFF_1:def 1;

assume A103: a1 = a3 ; :: thesis: a1,b2 // a2,b3

then a1,b1 // a1,b3 by A18, ANALMETR:59;

then a19,b19 // a19,b39 by ANALMETR:36;

hence a1,b2 // a2,b3 by A17, A103, A100, A102, AFF_1:14; :: thesis: verum