let X be OrtAfPl; :: thesis: ( X is satisfying_OSCH & X is satisfying_TDES implies X is satisfying_SCH )

assume that

A1: X is satisfying_OSCH and

A2: X is satisfying_TDES ; :: thesis: X is satisfying_SCH

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

for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4

let a2, a3, a4, b1, b2, b3, b4 be Element of X; :: thesis: for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4

let M, N be Subset of X; :: thesis: ( M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )

assume that

A3: M is being_line and

A4: N is being_line and

A5: a1 in M and

A6: a3 in M and

A7: b1 in M and

A8: b3 in M and

A9: a2 in N and

A10: a4 in N and

A11: b2 in N and

A12: b4 in N and

A13: not a4 in M and

A14: not a2 in M and

A15: not b2 in M and

A16: not b4 in M and

A17: not a1 in N and

A18: not a3 in N and

A19: not b1 in N and

A20: not b3 in N and

A21: a3,a2 // b3,b2 and

A22: a2,a1 // b2,b1 and

A23: a1,a4 // b1,b4 ; :: thesis: a3,a4 // b3,b4

reconsider a19 = a1, a29 = a2, a39 = a3, a49 = a4, b19 = b1, b29 = b2, b39 = b3, b49 = b4 as Element of 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 #) ;

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

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

A26: ( a1 <> b1 implies ( a2 <> b2 & a3 <> b3 & a4 <> b4 ) )

assume that

A1: X is satisfying_OSCH and

A2: X is satisfying_TDES ; :: thesis: X is satisfying_SCH

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

for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4

let a2, a3, a4, b1, b2, b3, b4 be Element of X; :: thesis: for M, N being Subset of X st M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 holds

a3,a4 // b3,b4

let M, N be Subset of X; :: thesis: ( M is being_line & N is being_line & a1 in M & a3 in M & b1 in M & b3 in M & a2 in N & a4 in N & b2 in N & b4 in N & not a4 in M & not a2 in M & not b2 in M & not b4 in M & not a1 in N & not a3 in N & not b1 in N & not b3 in N & a3,a2 // b3,b2 & a2,a1 // b2,b1 & a1,a4 // b1,b4 implies a3,a4 // b3,b4 )

assume that

A3: M is being_line and

A4: N is being_line and

A5: a1 in M and

A6: a3 in M and

A7: b1 in M and

A8: b3 in M and

A9: a2 in N and

A10: a4 in N and

A11: b2 in N and

A12: b4 in N and

A13: not a4 in M and

A14: not a2 in M and

A15: not b2 in M and

A16: not b4 in M and

A17: not a1 in N and

A18: not a3 in N and

A19: not b1 in N and

A20: not b3 in N and

A21: a3,a2 // b3,b2 and

A22: a2,a1 // b2,b1 and

A23: a1,a4 // b1,b4 ; :: thesis: a3,a4 // b3,b4

reconsider a19 = a1, a29 = a2, a39 = a3, a49 = a4, b19 = b1, b29 = b2, b39 = b3, b49 = b4 as Element of 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 #) ;

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

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

A26: ( a1 <> b1 implies ( a2 <> b2 & a3 <> b3 & a4 <> b4 ) )

proof

assume A27:
a1 <> b1
; :: thesis: ( a2 <> b2 & a3 <> b3 & a4 <> b4 )

hence contradiction by A29, A28, A30; :: thesis: verum

end;A28: now :: thesis: not a4 = b4

assume
a4 = b4
; :: thesis: contradiction

then a4,a1 // a4,b1 by A23, ANALMETR:59;

then LIN a4,a1,b1 by ANALMETR:def 10;

then LIN a49,a19,b19 by ANALMETR:40;

then LIN a19,b19,a49 by AFF_1:6;

hence contradiction by A5, A7, A13, A24, A27, AFF_1:25; :: thesis: verum

end;then a4,a1 // a4,b1 by A23, ANALMETR:59;

then LIN a4,a1,b1 by ANALMETR:def 10;

then LIN a49,a19,b19 by ANALMETR:40;

then LIN a19,b19,a49 by AFF_1:6;

hence contradiction by A5, A7, A13, A24, A27, AFF_1:25; :: thesis: verum

A29: now :: thesis: not a2 = b2

assume
a2 = b2
; :: thesis: contradiction

then LIN a2,a1,b1 by A22, ANALMETR:def 10;

then LIN a29,a19,b19 by ANALMETR:40;

then LIN a19,b19,a29 by AFF_1:6;

hence contradiction by A5, A7, A14, A24, A27, AFF_1:25; :: thesis: verum

end;then LIN a2,a1,b1 by A22, ANALMETR:def 10;

then LIN a29,a19,b19 by ANALMETR:40;

then LIN a19,b19,a29 by AFF_1:6;

hence contradiction by A5, A7, A14, A24, A27, AFF_1:25; :: thesis: verum

A30: now :: thesis: not a3 = b3

assume
( a2 = b2 or a3 = b3 or a4 = b4 )
; :: thesis: contradictionassume
a3 = b3
; :: thesis: contradiction

then LIN a3,a2,b2 by A21, ANALMETR:def 10;

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

then LIN a29,b29,a39 by AFF_1:6;

hence contradiction by A9, A11, A18, A25, A29, AFF_1:25; :: thesis: verum

end;then LIN a3,a2,b2 by A21, ANALMETR:def 10;

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

then LIN a29,b29,a39 by AFF_1:6;

hence contradiction by A9, A11, A18, A25, A29, AFF_1:25; :: thesis: verum

hence contradiction by A29, A28, A30; :: thesis: verum

A31: now :: thesis: ( a1 <> b1 implies a3,a4 // b3,b4 )

A140:
( a1 = b1 implies ( a2 = b2 & a3 = b3 & a4 = b4 ) )
assume A32:
a1 <> b1
; :: thesis: a3,a4 // b3,b4

end;A33: now :: thesis: ( a2 = a4 implies a3,a4 // b3,b4 )

A34:
not LIN a29,b19,b29

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

then b2,b1 // b1,b4 by A5, A14, A22, ANALMETR:60;

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

then A36: b19,b29 // b19,b49 by ANALMETR:36;

a29,b29 // a29,b49 by A9, A11, A12, A25, AFF_1:39, AFF_1:41;

then LIN a29,b29,b49 by AFF_1:def 1;

hence a3,a4 // b3,b4 by A21, A35, A34, A36, AFF_1:14; :: thesis: verum

end;proof

assume A35:
a2 = a4
; :: thesis: a3,a4 // b3,b4
assume
LIN a29,b19,b29
; :: thesis: contradiction

then LIN a29,b29,b19 by AFF_1:6;

hence contradiction by A9, A11, A19, A25, A26, A32, AFF_1:25; :: thesis: verum

end;then LIN a29,b29,b19 by AFF_1:6;

hence contradiction by A9, A11, A19, A25, A26, A32, AFF_1:25; :: thesis: verum

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

then b2,b1 // b1,b4 by A5, A14, A22, ANALMETR:60;

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

then A36: b19,b29 // b19,b49 by ANALMETR:36;

a29,b29 // a29,b49 by A9, A11, A12, A25, AFF_1:39, AFF_1:41;

then LIN a29,b29,b49 by AFF_1:def 1;

hence a3,a4 // b3,b4 by A21, A35, A34, A36, AFF_1:14; :: thesis: verum

A37: now :: thesis: ( a2 <> a4 & a1 <> a3 implies a3,a4 // b3,b4 )

assume that

A38: a2 <> a4 and

A39: a1 <> a3 ; :: thesis: a3,a4 // b3,b4

end;A38: a2 <> a4 and

A39: a1 <> a3 ; :: thesis: a3,a4 // b3,b4

A40: now :: thesis: ( M // N implies a3,a4 // b3,b4 )

consider e1 being Element of X such that

A41: b1,b2 // b1,e1 and

A42: b1 <> e1 by ANALMETR:39;

consider x being Element of X such that

A43: LIN a1,a2,x and

A44: a1 <> x and

A45: a2 <> x by Th2;

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

consider e2 being Element of X such that

A46: a1,b1 // x,e2 and

A47: x <> e2 by ANALMETR:39;

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

not b19,e19 // x9,e29

A48: LIN b19,e19,y9 and

A49: LIN x9,e29,y9 by AFF_1:60;

reconsider y = y9 as Element of X ;

A50: a1,a2 // a1,x by A43, ANALMETR:def 10;

A51: not LIN a2,b2,x

then M9 // N9 by ANALMETR:46;

then a39,b39 // a29,b29 by A6, A8, A9, A11, AFF_1:39;

then a3,b3 // a2,b2 by ANALMETR:36;

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

LIN x,e2,y by A49, ANALMETR:40;

then x,e2 // x,y by ANALMETR:def 10;

then A59: a1,b1 // x,y by A46, A47, ANALMETR:60;

A60: b1 <> y

then b1,e1 // b1,y by ANALMETR:def 10;

then A62: b1,b2 // b1,y by A41, A42, ANALMETR:60;

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

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

then LIN y9,b19,b29 by AFF_1:6;

then LIN y,b1,b2 by ANALMETR:40;

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

then A63: b1,y // b2,y by ANALMETR:59;

a1,a2 // b1,b2 by A22, ANALMETR:59;

then a1,a2 // b1,y by A7, A15, A62, ANALMETR:60;

then A64: a1,x // b1,y by A5, A14, A50, ANALMETR:60;

A65: not LIN x,y,a3

then LIN x9,a19,a29 by AFF_1:6;

then LIN x,a1,a2 by ANALMETR:40;

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

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

then a2,x // b1,y by A44, A64, ANALMETR:60;

then A78: a2,x // b2,y by A60, A63, ANALMETR:60;

a19,b19 // a39,b39 by A5, A6, A7, A8, A24, AFF_1:39, AFF_1:41;

then a1,b1 // a3,b3 by ANALMETR:36;

then A79: x,y // a3,b3 by A32, A59, ANALMETR:60;

M9 // N9 by A57, ANALMETR:46;

then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;

then a1,b1 // a4,b4 by ANALMETR:36;

then A80: x,y // a4,b4 by A32, A59, ANALMETR:60;

M9 // N9 by A57, ANALMETR:46;

then a19,b19 // a29,b29 by A5, A7, A9, A11, AFF_1:39;

then a1,b1 // a2,b2 by ANALMETR:36;

then A81: a2,b2 // x,y by A32, A59, ANALMETR:60;

a2,a3 // b2,b3 by A21, ANALMETR:59;

then A82: x,a3 // y,b3 by A2, A77, A51, A75, A81, A58, A78;

M9 // N9 by A57, ANALMETR:46;

then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;

then a1,b1 // a4,b4 by ANALMETR:36;

then x,a4 // y,b4 by A2, A23, A59, A77, A55, A54, A64;

hence a3,a4 // b3,b4 by A2, A77, A82, A65, A70, A79, A80; :: thesis: verum

end;A41: b1,b2 // b1,e1 and

A42: b1 <> e1 by ANALMETR:39;

consider x being Element of X such that

A43: LIN a1,a2,x and

A44: a1 <> x and

A45: a2 <> x by Th2;

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

consider e2 being Element of X such that

A46: a1,b1 // x,e2 and

A47: x <> e2 by ANALMETR:39;

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

not b19,e19 // x9,e29

proof

then consider y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
assume
b19,e19 // x9,e29
; :: thesis: contradiction

then b1,e1 // x,e2 by ANALMETR:36;

then b1,b2 // x,e2 by A41, A42, ANALMETR:60;

then b1,b2 // a1,b1 by A46, A47, ANALMETR:60;

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

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

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

hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; :: thesis: verum

end;then b1,e1 // x,e2 by ANALMETR:36;

then b1,b2 // x,e2 by A41, A42, ANALMETR:60;

then b1,b2 // a1,b1 by A46, A47, ANALMETR:60;

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

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

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

hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; :: thesis: verum

A48: LIN b19,e19,y9 and

A49: LIN x9,e29,y9 by AFF_1:60;

reconsider y = y9 as Element of X ;

A50: a1,a2 // a1,x by A43, ANALMETR:def 10;

A51: not LIN a2,b2,x

proof

A54:
not LIN a1,b1,a4
A52:
a2 <> b2

then A53: LIN a29,x9,a19 by AFF_1:6;

assume LIN a2,b2,x ; :: thesis: contradiction

then LIN a29,b29,x9 by ANALMETR:40;

then x9 in N9 by A9, A11, A25, A52, AFF_1:25;

hence contradiction by A9, A17, A25, A45, A53, AFF_1:25; :: thesis: verum

end;proof

LIN a19,a29,x9
by A43, ANALMETR:40;
assume
a2 = b2
; :: thesis: contradiction

then LIN a2,a1,b1 by A22, ANALMETR:def 10;

then LIN a29,a19,b19 by ANALMETR:40;

then LIN a19,b19,a29 by AFF_1:6;

hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum

end;then LIN a2,a1,b1 by A22, ANALMETR:def 10;

then LIN a29,a19,b19 by ANALMETR:40;

then LIN a19,b19,a29 by AFF_1:6;

hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum

then A53: LIN a29,x9,a19 by AFF_1:6;

assume LIN a2,b2,x ; :: thesis: contradiction

then LIN a29,b29,x9 by ANALMETR:40;

then x9 in N9 by A9, A11, A25, A52, AFF_1:25;

hence contradiction by A9, A17, A25, A45, A53, AFF_1:25; :: thesis: verum

proof

A55:
not LIN a1,b1,x
assume
LIN a1,b1,a4
; :: thesis: contradiction

then LIN a19,b19,a49 by ANALMETR:40;

hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; :: thesis: verum

end;then LIN a19,b19,a49 by ANALMETR:40;

hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; :: thesis: verum

proof

assume A57:
M // N
; :: thesis: a3,a4 // b3,b4
assume
LIN a1,b1,x
; :: thesis: contradiction

then LIN a19,b19,x9 by ANALMETR:40;

then A56: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a19,x9,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A56, AFF_1:25; :: thesis: verum

end;then LIN a19,b19,x9 by ANALMETR:40;

then A56: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a19,x9,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A56, AFF_1:25; :: thesis: verum

then M9 // N9 by ANALMETR:46;

then a39,b39 // a29,b29 by A6, A8, A9, A11, AFF_1:39;

then a3,b3 // a2,b2 by ANALMETR:36;

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

LIN x,e2,y by A49, ANALMETR:40;

then x,e2 // x,y by ANALMETR:def 10;

then A59: a1,b1 // x,y by A46, A47, ANALMETR:60;

A60: b1 <> y

proof

LIN b1,e1,y
by A48, ANALMETR:40;
assume
b1 = y
; :: thesis: contradiction

then b1,a1 // b1,x by A59, ANALMETR:59;

then LIN b1,a1,x by ANALMETR:def 10;

then LIN b19,a19,x9 by ANALMETR:40;

then A61: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a19,x9,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A61, AFF_1:25; :: thesis: verum

end;then b1,a1 // b1,x by A59, ANALMETR:59;

then LIN b1,a1,x by ANALMETR:def 10;

then LIN b19,a19,x9 by ANALMETR:40;

then A61: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a19,x9,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A61, AFF_1:25; :: thesis: verum

then b1,e1 // b1,y by ANALMETR:def 10;

then A62: b1,b2 // b1,y by A41, A42, ANALMETR:60;

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

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

then LIN y9,b19,b29 by AFF_1:6;

then LIN y,b1,b2 by ANALMETR:40;

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

then A63: b1,y // b2,y by ANALMETR:59;

a1,a2 // b1,b2 by A22, ANALMETR:59;

then a1,a2 // b1,y by A7, A15, A62, ANALMETR:60;

then A64: a1,x // b1,y by A5, A14, A50, ANALMETR:60;

A65: not LIN x,y,a3

proof

A70:
not LIN x,y,a4
A66:
x <> y

then a1,a3 // a1,b1 by ANALMETR:36;

then A68: x,y // a1,a3 by A32, A59, ANALMETR:60;

assume LIN x,y,a3 ; :: thesis: contradiction

then x,y // x,a3 by ANALMETR:def 10;

then x,a3 // a1,a3 by A66, A68, ANALMETR:60;

then a3,a1 // a3,x by ANALMETR:59;

then LIN a3,a1,x by ANALMETR:def 10;

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

then A69: x9 in M9 by A5, A6, A24, A39, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a19,x9,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A69, AFF_1:25; :: thesis: verum

end;proof

a19,a39 // a19,b19
by A5, A6, A7, A24, AFF_1:39, AFF_1:41;
assume
x = y
; :: thesis: contradiction

then x,a1 // x,b1 by A64, ANALMETR:59;

then LIN x,a1,b1 by ANALMETR:def 10;

then LIN x9,a19,b19 by ANALMETR:40;

then LIN a19,b19,x9 by AFF_1:6;

then A67: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN x9,a19,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A67, AFF_1:25; :: thesis: verum

end;then x,a1 // x,b1 by A64, ANALMETR:59;

then LIN x,a1,b1 by ANALMETR:def 10;

then LIN x9,a19,b19 by ANALMETR:40;

then LIN a19,b19,x9 by AFF_1:6;

then A67: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN x9,a19,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A67, AFF_1:25; :: thesis: verum

then a1,a3 // a1,b1 by ANALMETR:36;

then A68: x,y // a1,a3 by A32, A59, ANALMETR:60;

assume LIN x,y,a3 ; :: thesis: contradiction

then x,y // x,a3 by ANALMETR:def 10;

then x,a3 // a1,a3 by A66, A68, ANALMETR:60;

then a3,a1 // a3,x by ANALMETR:59;

then LIN a3,a1,x by ANALMETR:def 10;

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

then A69: x9 in M9 by A5, A6, A24, A39, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a19,x9,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A69, AFF_1:25; :: thesis: verum

proof

A75:
not LIN a2,b2,a3
A71:
x <> y

then a19,b19 // a29,a49 by A5, A7, A9, A10, AFF_1:39;

then a1,b1 // a2,a4 by ANALMETR:36;

then A73: a2,a4 // x,y by A32, A59, ANALMETR:60;

assume LIN x,y,a4 ; :: thesis: contradiction

then x,y // x,a4 by ANALMETR:def 10;

then a2,a4 // x,a4 by A71, A73, ANALMETR:60;

then a4,a2 // a4,x by ANALMETR:59;

then LIN a4,a2,x by ANALMETR:def 10;

then LIN a49,a29,x9 by ANALMETR:40;

then A74: x9 in N9 by A9, A10, A25, A38, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a29,x9,a19 by AFF_1:6;

hence contradiction by A9, A17, A25, A45, A74, AFF_1:25; :: thesis: verum

end;proof

M9 // N9
by A57, ANALMETR:46;
assume
x = y
; :: thesis: contradiction

then x,a1 // x,b1 by A64, ANALMETR:59;

then LIN x,a1,b1 by ANALMETR:def 10;

then LIN x9,a19,b19 by ANALMETR:40;

then LIN a19,b19,x9 by AFF_1:6;

then A72: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN x9,a19,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A72, AFF_1:25; :: thesis: verum

end;then x,a1 // x,b1 by A64, ANALMETR:59;

then LIN x,a1,b1 by ANALMETR:def 10;

then LIN x9,a19,b19 by ANALMETR:40;

then LIN a19,b19,x9 by AFF_1:6;

then A72: x9 in M9 by A5, A7, A24, A32, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN x9,a19,a29 by AFF_1:6;

hence contradiction by A5, A14, A24, A44, A72, AFF_1:25; :: thesis: verum

then a19,b19 // a29,a49 by A5, A7, A9, A10, AFF_1:39;

then a1,b1 // a2,a4 by ANALMETR:36;

then A73: a2,a4 // x,y by A32, A59, ANALMETR:60;

assume LIN x,y,a4 ; :: thesis: contradiction

then x,y // x,a4 by ANALMETR:def 10;

then a2,a4 // x,a4 by A71, A73, ANALMETR:60;

then a4,a2 // a4,x by ANALMETR:59;

then LIN a4,a2,x by ANALMETR:def 10;

then LIN a49,a29,x9 by ANALMETR:40;

then A74: x9 in N9 by A9, A10, A25, A38, AFF_1:25;

LIN a19,a29,x9 by A43, ANALMETR:40;

then LIN a29,x9,a19 by AFF_1:6;

hence contradiction by A9, A17, A25, A45, A74, AFF_1:25; :: thesis: verum

proof

A77:
( X is satisfying_TDES implies X is satisfying_des )
A76:
a2 <> b2

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

hence contradiction by A9, A11, A18, A25, A76, AFF_1:25; :: thesis: verum

end;proof

assume
LIN a2,b2,a3
; :: thesis: contradiction
assume
a2 = b2
; :: thesis: contradiction

then LIN a2,a1,b1 by A22, ANALMETR:def 10;

then LIN a29,a19,b19 by ANALMETR:40;

then LIN a19,b19,a29 by AFF_1:6;

hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum

end;then LIN a2,a1,b1 by A22, ANALMETR:def 10;

then LIN a29,a19,b19 by ANALMETR:40;

then LIN a19,b19,a29 by AFF_1:6;

hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum

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

hence contradiction by A9, A11, A18, A25, A76, AFF_1:25; :: thesis: verum

proof

LIN a19,a29,x9
by A43, ANALMETR:40;
assume
X is satisfying_TDES
; :: thesis: X is satisfying_des

then AffinStruct(# the carrier of X, the CONGR of X #) is Moufangian by Th7;

then AffinStruct(# the carrier of X, the CONGR of X #) is translational by AFF_2:14;

hence X is satisfying_des by Th8; :: thesis: verum

end;then AffinStruct(# the carrier of X, the CONGR of X #) is Moufangian by Th7;

then AffinStruct(# the carrier of X, the CONGR of X #) is translational by AFF_2:14;

hence X is satisfying_des by Th8; :: thesis: verum

then LIN x9,a19,a29 by AFF_1:6;

then LIN x,a1,a2 by ANALMETR:40;

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

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

then a2,x // b1,y by A44, A64, ANALMETR:60;

then A78: a2,x // b2,y by A60, A63, ANALMETR:60;

a19,b19 // a39,b39 by A5, A6, A7, A8, A24, AFF_1:39, AFF_1:41;

then a1,b1 // a3,b3 by ANALMETR:36;

then A79: x,y // a3,b3 by A32, A59, ANALMETR:60;

M9 // N9 by A57, ANALMETR:46;

then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;

then a1,b1 // a4,b4 by ANALMETR:36;

then A80: x,y // a4,b4 by A32, A59, ANALMETR:60;

M9 // N9 by A57, ANALMETR:46;

then a19,b19 // a29,b29 by A5, A7, A9, A11, AFF_1:39;

then a1,b1 // a2,b2 by ANALMETR:36;

then A81: a2,b2 // x,y by A32, A59, ANALMETR:60;

a2,a3 // b2,b3 by A21, ANALMETR:59;

then A82: x,a3 // y,b3 by A2, A77, A51, A75, A81, A58, A78;

M9 // N9 by A57, ANALMETR:46;

then a19,b19 // a49,b49 by A5, A7, A10, A12, AFF_1:39;

then a1,b1 // a4,b4 by ANALMETR:36;

then x,a4 // y,b4 by A2, A23, A59, A77, A55, A54, A64;

hence a3,a4 // b3,b4 by A2, A77, A82, A65, A70, A79, A80; :: thesis: verum

now :: thesis: ( not M // N implies a3,a4 // b3,b4 )

hence
a3,a4 // b3,b4
by A40; :: thesis: verumassume
not M // N
; :: thesis: a3,a4 // b3,b4

then not M9 // N9 by ANALMETR:46;

then consider o9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A83: o9 in M9 and

A84: o9 in N9 by A24, A25, AFF_1:58;

reconsider o = o9 as Element of X ;

consider K being Subset of X such that

A85: o in K and

A86: N _|_ K by A4, Th3;

reconsider K9 = K as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;

A87: K is being_line by A86, ANALMETR:44;

then A88: K9 is being_line by ANALMETR:43;

end;then not M9 // N9 by ANALMETR:46;

then consider o9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A83: o9 in M9 and

A84: o9 in N9 by A24, A25, AFF_1:58;

reconsider o = o9 as Element of X ;

consider K being Subset of X such that

A85: o in K and

A86: N _|_ K by A4, Th3;

reconsider K9 = K as Subset of AffinStruct(# the carrier of X, the CONGR of X #) ;

A87: K is being_line by A86, ANALMETR:44;

then A88: K9 is being_line by ANALMETR:43;

now :: thesis: ( K <> M implies a3,a4 // b3,b4 )

hence
a3,a4 // b3,b4
by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, A23, A86; :: thesis: verumA89:
( not a2 in K & not a4 in K & not b2 in K & not b4 in K )

A103: d19 in K9 and

A104: a19,d19 // N9 ;

consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A105: e19 in K9 and

A106: b19,e19 // N9 by A98;

consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A107: d39 in K9 and

A108: a39,d39 // N9 by A98;

consider e39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A109: e39 in K9 and

A110: b39,e39 // N9 by A98;

reconsider d1 = d19, d3 = d39, e1 = e19, e3 = e39 as Element of X ;

A111: LIN o,d1,e1 by A85, A87, A103, A105, Th4;

A112: ( o <> e1 & o <> e3 & o <> d1 & o <> d3 )

then A118: d1,a1 // o,a2 by ANALMETR:59;

A119: not e1 in N by A19, A106, AFF_1:35;

A120: not d3 in N by A18, A108, AFF_1:35;

a19,d19 // b19,e19 by A25, A104, A106, AFF_1:31;

then a1,d1 // b1,e1 by ANALMETR:36;

then A121: d1,a1 // e1,b1 by ANALMETR:59;

assume A122: K <> M ; :: thesis: a3,a4 // b3,b4

then A125: a3,d3 // b3,e3 by ANALMETR:36;

then A126: d3,a3 // e3,b3 by ANALMETR:59;

A127: ( not LIN d3,e3,a3 & not LIN d3,e3,a4 )

a1,a2 // b1,b2 by A22, ANALMETR:59;

then d1,a2 // e1,b2 by A2, A14, A15, A17, A19, A83, A84, A112, A93, A97, A111, A124, A129, A121, A118;

then A131: a2,d1 // b2,e1 by ANALMETR:59;

A132: not e3 in N by A20, A110, AFF_1:35;

A133: LIN o,d3,e3 by A85, A87, A107, A109, Th4;

a1,d1 // o,a4 by A10, A84, A104, Th6;

then d1,a1 // o,a4 by ANALMETR:59;

then A134: d1,a4 // e1,b4 by A2, A13, A16, A17, A19, A23, A83, A84, A112, A97, A130, A111, A124, A94, A121;

A135: a3,d3 // o,a4 by A10, A84, A108, Th6;

A136: not d1 in N by A17, A104, AFF_1:35;

a3,d3 // o,a2 by A9, A84, A108, Th6;

then d3,a3 // o,a2 by ANALMETR:59;

then d3,a2 // e3,b2 by A2, A14, A15, A18, A20, A21, A83, A84, A112, A93, A95, A133, A123, A96, A126;

then d3,a4 // e3,b4 by A1, A9, A10, A11, A12, A86, A103, A107, A109, A105, A131, A134, A136, A120, A119, A132, A89;

hence a3,a4 // b3,b4 by A2, A13, A16, A18, A20, A83, A84, A112, A130, A95, A133, A125, A127, A135; :: thesis: verum

end;proof

hence contradiction by A9, A10, A11, A12, A13, A14, A15, A16, A83, A90; :: thesis: verum

end;

A93:
LIN o,a2,b2
by A4, A9, A11, A84, Th4;A90: now :: thesis: for x being Element of X st x in N & o <> x holds

not x in K

assume
( a2 in K or a4 in K or b2 in K or b4 in K )
; :: thesis: contradictionnot x in K

let x be Element of X; :: thesis: ( x in N & o <> x implies not x in K )

assume that

A91: x in N and

A92: o <> x ; :: thesis: not x in K

assume x in K ; :: thesis: contradiction

then o,x _|_ o,x by A84, A85, A86, A91, ANALMETR:56;

hence contradiction by A92, ANALMETR:39; :: thesis: verum

end;assume that

A91: x in N and

A92: o <> x ; :: thesis: not x in K

assume x in K ; :: thesis: contradiction

then o,x _|_ o,x by A84, A85, A86, A91, ANALMETR:56;

hence contradiction by A92, ANALMETR:39; :: thesis: verum

hence contradiction by A9, A10, A11, A12, A13, A14, A15, A16, A83, A90; :: thesis: verum

A94: now :: thesis: not LIN a1,b1,a4

A95:
LIN o,a3,b3
by A3, A6, A8, A83, Th4;assume
LIN a1,b1,a4
; :: thesis: contradiction

then LIN a19,b19,a49 by ANALMETR:40;

hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; :: thesis: verum

end;then LIN a19,b19,a49 by ANALMETR:40;

hence contradiction by A5, A7, A13, A24, A32, AFF_1:25; :: thesis: verum

A96: now :: thesis: not LIN a3,b3,a2

A97:
LIN o,a1,b1
by A3, A5, A7, A83, Th4;assume
LIN a3,b3,a2
; :: thesis: contradiction

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

hence contradiction by A6, A8, A14, A24, A26, A32, AFF_1:25; :: thesis: verum

end;then LIN a39,b39,a29 by ANALMETR:40;

hence contradiction by A6, A8, A14, A24, A26, A32, AFF_1:25; :: thesis: verum

A98: now :: thesis: for x9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) ex y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st

( y9 in K9 & x9,y9 // N9 )

then consider d19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that ( y9 in K9 & x9,y9 // N9 )

let x9 be Element of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: ex y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st

( y9 in K9 & x9,y9 // N9 )

consider D9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that

A99: x9 in D9 and

A100: N9 // D9 by A25, AFF_1:49;

reconsider D = D9 as Subset of the carrier of X ;

N // D by A100, ANALMETR:46;

then K _|_ D by A86, ANALMETR:52;

then consider y being Element of X such that

A101: y in K and

A102: y in D by ANALMETR:66;

reconsider y9 = y as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

take y9 = y9; :: thesis: ( y9 in K9 & x9,y9 // N9 )

thus ( y9 in K9 & x9,y9 // N9 ) by A99, A100, A101, A102, AFF_1:40; :: thesis: verum

end;( y9 in K9 & x9,y9 // N9 )

consider D9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that

A99: x9 in D9 and

A100: N9 // D9 by A25, AFF_1:49;

reconsider D = D9 as Subset of the carrier of X ;

N // D by A100, ANALMETR:46;

then K _|_ D by A86, ANALMETR:52;

then consider y being Element of X such that

A101: y in K and

A102: y in D by ANALMETR:66;

reconsider y9 = y as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

take y9 = y9; :: thesis: ( y9 in K9 & x9,y9 // N9 )

thus ( y9 in K9 & x9,y9 // N9 ) by A99, A100, A101, A102, AFF_1:40; :: thesis: verum

A103: d19 in K9 and

A104: a19,d19 // N9 ;

consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A105: e19 in K9 and

A106: b19,e19 // N9 by A98;

consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A107: d39 in K9 and

A108: a39,d39 // N9 by A98;

consider e39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that

A109: e39 in K9 and

A110: b39,e39 // N9 by A98;

reconsider d1 = d19, d3 = d39, e1 = e19, e3 = e39 as Element of X ;

A111: LIN o,d1,e1 by A85, A87, A103, A105, Th4;

A112: ( o <> e1 & o <> e3 & o <> d1 & o <> d3 )

proof

hence contradiction by A5, A6, A7, A8, A17, A18, A19, A20, A103, A104, A107, A108, A109, A110, A105, A106, A113; :: thesis: verum

end;

a1,d1 // o,a2
by A9, A84, A104, Th6;A113: now :: thesis: for x, y being Element of X

for x9, y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N holds

not o = y

assume
( not o <> e1 or not o <> e3 or not o <> d1 or not o <> d3 )
; :: thesis: contradictionfor x9, y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N holds

not o = y

let x, y be Element of X; :: thesis: for x9, y9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N holds

not o = y

let x9, y9 be Element of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: ( x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N implies not o = y )

assume that

A114: x9,y9 // N9 and

A115: x = x9 and

A116: y = y9 and

x in M and

y in K and

A117: not x in N ; :: thesis: not o = y

assume o = y ; :: thesis: contradiction

then o9,x9 // N9 by A114, A116, AFF_1:34;

hence contradiction by A25, A84, A115, A117, AFF_1:23; :: thesis: verum

end;not o = y

let x9, y9 be Element of AffinStruct(# the carrier of X, the CONGR of X #); :: thesis: ( x9,y9 // N9 & x = x9 & y = y9 & x in M & y in K & not x in N implies not o = y )

assume that

A114: x9,y9 // N9 and

A115: x = x9 and

A116: y = y9 and

x in M and

y in K and

A117: not x in N ; :: thesis: not o = y

assume o = y ; :: thesis: contradiction

then o9,x9 // N9 by A114, A116, AFF_1:34;

hence contradiction by A25, A84, A115, A117, AFF_1:23; :: thesis: verum

hence contradiction by A5, A6, A7, A8, A17, A18, A19, A20, A103, A104, A107, A108, A109, A110, A105, A106, A113; :: thesis: verum

then A118: d1,a1 // o,a2 by ANALMETR:59;

A119: not e1 in N by A19, A106, AFF_1:35;

A120: not d3 in N by A18, A108, AFF_1:35;

a19,d19 // b19,e19 by A25, A104, A106, AFF_1:31;

then a1,d1 // b1,e1 by ANALMETR:36;

then A121: d1,a1 // e1,b1 by ANALMETR:59;

assume A122: K <> M ; :: thesis: a3,a4 // b3,b4

A123: now :: thesis: not LIN a3,b3,d3

assume
LIN a3,b3,d3
; :: thesis: contradiction

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

then d3 in M by A6, A8, A24, A26, A32, AFF_1:25;

hence contradiction by A3, A83, A85, A87, A122, A107, A112, Th5; :: thesis: verum

end;then LIN a39,b39,d39 by ANALMETR:40;

then d3 in M by A6, A8, A24, A26, A32, AFF_1:25;

hence contradiction by A3, A83, A85, A87, A122, A107, A112, Th5; :: thesis: verum

A124: now :: thesis: not LIN a1,b1,d1

a39,d39 // b39,e39
by A25, A108, A110, AFF_1:31;assume
LIN a1,b1,d1
; :: thesis: contradiction

then LIN a19,b19,d19 by ANALMETR:40;

then d1 in M by A5, A7, A24, A32, AFF_1:25;

hence contradiction by A3, A83, A85, A87, A122, A103, A112, Th5; :: thesis: verum

end;then LIN a19,b19,d19 by ANALMETR:40;

then d1 in M by A5, A7, A24, A32, AFF_1:25;

hence contradiction by A3, A83, A85, A87, A122, A103, A112, Th5; :: thesis: verum

then A125: a3,d3 // b3,e3 by ANALMETR:36;

then A126: d3,a3 // e3,b3 by ANALMETR:59;

A127: ( not LIN d3,e3,a3 & not LIN d3,e3,a4 )

proof

A128:
d3 <> e3

then ( LIN d39,e39,a39 or LIN d39,e39,a49 ) by ANALMETR:40;

then ( a39 in K9 or a49 in K9 ) by A88, A107, A109, A128, AFF_1:25;

hence contradiction by A6, A10, A13, A18, A24, A25, A83, A84, A85, A86, A88, A122, AFF_1:18; :: thesis: verum

end;proof

assume
( LIN d3,e3,a3 or LIN d3,e3,a4 )
; :: thesis: contradiction
assume
not d3 <> e3
; :: thesis: contradiction

then LIN e3,a3,b3 by A126, ANALMETR:def 10;

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

then LIN a39,b39,e39 by AFF_1:6;

then e39 in M9 by A6, A8, A24, A26, A32, AFF_1:25;

hence contradiction by A24, A83, A85, A88, A122, A109, A112, AFF_1:18; :: thesis: verum

end;then LIN e3,a3,b3 by A126, ANALMETR:def 10;

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

then LIN a39,b39,e39 by AFF_1:6;

then e39 in M9 by A6, A8, A24, A26, A32, AFF_1:25;

hence contradiction by A24, A83, A85, A88, A122, A109, A112, AFF_1:18; :: thesis: verum

then ( LIN d39,e39,a39 or LIN d39,e39,a49 ) by ANALMETR:40;

then ( a39 in K9 or a49 in K9 ) by A88, A107, A109, A128, AFF_1:25;

hence contradiction by A6, A10, A13, A18, A24, A25, A83, A84, A85, A86, A88, A122, AFF_1:18; :: thesis: verum

A129: now :: thesis: not LIN a1,b1,a2

A130:
LIN o,a4,b4
by A4, A10, A12, A84, Th4;assume
LIN a1,b1,a2
; :: thesis: contradiction

then LIN a19,b19,a29 by ANALMETR:40;

hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum

end;then LIN a19,b19,a29 by ANALMETR:40;

hence contradiction by A5, A7, A14, A24, A32, AFF_1:25; :: thesis: verum

a1,a2 // b1,b2 by A22, ANALMETR:59;

then d1,a2 // e1,b2 by A2, A14, A15, A17, A19, A83, A84, A112, A93, A97, A111, A124, A129, A121, A118;

then A131: a2,d1 // b2,e1 by ANALMETR:59;

A132: not e3 in N by A20, A110, AFF_1:35;

A133: LIN o,d3,e3 by A85, A87, A107, A109, Th4;

a1,d1 // o,a4 by A10, A84, A104, Th6;

then d1,a1 // o,a4 by ANALMETR:59;

then A134: d1,a4 // e1,b4 by A2, A13, A16, A17, A19, A23, A83, A84, A112, A97, A130, A111, A124, A94, A121;

A135: a3,d3 // o,a4 by A10, A84, A108, Th6;

A136: not d1 in N by A17, A104, AFF_1:35;

a3,d3 // o,a2 by A9, A84, A108, Th6;

then d3,a3 // o,a2 by ANALMETR:59;

then d3,a2 // e3,b2 by A2, A14, A15, A18, A20, A21, A83, A84, A112, A93, A95, A133, A123, A96, A126;

then d3,a4 // e3,b4 by A1, A9, A10, A11, A12, A86, A103, A107, A109, A105, A131, A134, A136, A120, A119, A132, A89;

hence a3,a4 // b3,b4 by A2, A13, A16, A18, A20, A83, A84, A112, A130, A95, A133, A125, A127, A135; :: thesis: verum

now :: thesis: ( a1 = a3 implies a3,a4 // b3,b4 )

hence
a3,a4 // b3,b4
by A33, A37; :: thesis: verumA137:
not LIN a19,b29,b19

then A138: LIN a19,b19,b39 by AFF_1:def 1;

assume A139: a1 = a3 ; :: thesis: a3,a4 // b3,b4

then a2,a1 // b2,b3 by A21, ANALMETR:59;

then b2,b1 // b2,b3 by A5, A14, A22, ANALMETR:60;

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

hence a3,a4 // b3,b4 by A23, A139, A137, A138, AFF_1:14; :: thesis: verum

end;proof

a19,b19 // a19,b39
by A5, A7, A8, A24, AFF_1:39, AFF_1:41;
assume
LIN a19,b29,b19
; :: thesis: contradiction

then LIN a19,b19,b29 by AFF_1:6;

hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; :: thesis: verum

end;then LIN a19,b19,b29 by AFF_1:6;

hence contradiction by A5, A7, A15, A24, A32, AFF_1:25; :: thesis: verum

then A138: LIN a19,b19,b39 by AFF_1:def 1;

assume A139: a1 = a3 ; :: thesis: a3,a4 // b3,b4

then a2,a1 // b2,b3 by A21, ANALMETR:59;

then b2,b1 // b2,b3 by A5, A14, A22, ANALMETR:60;

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

hence a3,a4 // b3,b4 by A23, A139, A137, A138, AFF_1:14; :: thesis: verum

proof

assume A141:
a1 = b1
; :: thesis: ( a2 = b2 & a3 = b3 & a4 = b4 )

hence contradiction by A144, A142, A146; :: thesis: verum

end;A142: now :: thesis: not a4 <> b4

LIN a1,a4,b4
by A23, A141, ANALMETR:def 10;

then LIN a19,a49,b49 by ANALMETR:40;

then A143: LIN a49,b49,a19 by AFF_1:6;

assume a4 <> b4 ; :: thesis: contradiction

hence contradiction by A10, A12, A17, A25, A143, AFF_1:25; :: thesis: verum

end;then LIN a19,a49,b49 by ANALMETR:40;

then A143: LIN a49,b49,a19 by AFF_1:6;

assume a4 <> b4 ; :: thesis: contradiction

hence contradiction by A10, A12, A17, A25, A143, AFF_1:25; :: thesis: verum

A144: now :: thesis: not a2 <> b2

a1,a2 // a1,b2
by A22, A141, ANALMETR:59;

then LIN a1,a2,b2 by ANALMETR:def 10;

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

then A145: LIN a29,b29,a19 by AFF_1:6;

assume a2 <> b2 ; :: thesis: contradiction

hence contradiction by A9, A11, A17, A25, A145, AFF_1:25; :: thesis: verum

end;then LIN a1,a2,b2 by ANALMETR:def 10;

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

then A145: LIN a29,b29,a19 by AFF_1:6;

assume a2 <> b2 ; :: thesis: contradiction

hence contradiction by A9, A11, A17, A25, A145, AFF_1:25; :: thesis: verum

A146: now :: thesis: not a3 <> b3

assume
( a2 <> b2 or a3 <> b3 or a4 <> b4 )
; :: thesis: contradiction
a2,a3 // a2,b3
by A21, A144, ANALMETR:59;

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

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

then A147: LIN a39,b39,a29 by AFF_1:6;

assume a3 <> b3 ; :: thesis: contradiction

hence contradiction by A6, A8, A14, A24, A147, AFF_1:25; :: thesis: verum

end;then LIN a2,a3,b3 by ANALMETR:def 10;

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

then A147: LIN a39,b39,a29 by AFF_1:6;

assume a3 <> b3 ; :: thesis: contradiction

hence contradiction by A6, A8, A14, A24, A147, AFF_1:25; :: thesis: verum

hence contradiction by A144, A142, A146; :: thesis: verum

now :: thesis: ( a1 = b1 implies a3,a4 // b3,b4 )

hence
a3,a4 // b3,b4
by A31; :: thesis: verumassume
a1 = b1
; :: thesis: a3,a4 // b3,b4

then a39,a49 // b39,b49 by A140, AFF_1:2;

hence a3,a4 // b3,b4 by ANALMETR:36; :: thesis: verum

end;then a39,a49 // b39,b49 by A140, AFF_1:2;

hence a3,a4 // b3,b4 by ANALMETR:36; :: thesis: verum