let X be OrtAfPl; :: thesis: ( X is satisfying_MH2 implies X is satisfying_OSCH )

assume A1: X is satisfying_MH2 ; :: thesis: X is satisfying_OSCH

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

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

a3,a4 // b3,b4

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

a3,a4 // b3,b4

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

assume that

A2: M _|_ N and

A3: a1 in M and

A4: a3 in M and

A5: b1 in M and

A6: b3 in M and

A7: a2 in N and

A8: a4 in N and

A9: b2 in N and

A10: b4 in N and

A11: not a4 in M and

A12: not a2 in M and

A13: not b2 in M and

A14: not b4 in M and

A15: not a1 in N and

A16: not a3 in N and

A17: not b1 in N and

not b3 in N and

A18: a3,a2 // b3,b2 and

A19: a2,a1 // b2,b1 and

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

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

N is being_line by A2, ANALMETR:44;

then A21: N9 is being_line by ANALMETR:43;

reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

M is being_line by A2, ANALMETR:44;

then A22: M9 is being_line by ANALMETR:43;

not M9 // N9

( o9 in M9 & o9 in N9 ) by A22, A21, AFF_1:58;

then consider o being Element of X such that

A23: o in M and

A24: o in N ;

reconsider o9 = o as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

assume A1: X is satisfying_MH2 ; :: thesis: X is satisfying_OSCH

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

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

a3,a4 // b3,b4

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

a3,a4 // b3,b4

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

assume that

A2: M _|_ N and

A3: a1 in M and

A4: a3 in M and

A5: b1 in M and

A6: b3 in M and

A7: a2 in N and

A8: a4 in N and

A9: b2 in N and

A10: b4 in N and

A11: not a4 in M and

A12: not a2 in M and

A13: not b2 in M and

A14: not b4 in M and

A15: not a1 in N and

A16: not a3 in N and

A17: not b1 in N and

not b3 in N and

A18: a3,a2 // b3,b2 and

A19: a2,a1 // b2,b1 and

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

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

N is being_line by A2, ANALMETR:44;

then A21: N9 is being_line by ANALMETR:43;

reconsider b49 = b4, b19 = b1, b29 = b2, b39 = b3, a19 = a1, a29 = a2, a39 = a3, a49 = a4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

M is being_line by A2, ANALMETR:44;

then A22: M9 is being_line by ANALMETR:43;

not M9 // N9

proof

then
ex o9 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st
assume
M9 // N9
; :: thesis: contradiction

then M // N by ANALMETR:46;

hence contradiction by A2, ANALMETR:52; :: thesis: verum

end;then M // N by ANALMETR:46;

hence contradiction by A2, ANALMETR:52; :: thesis: verum

( o9 in M9 & o9 in N9 ) by A22, A21, AFF_1:58;

then consider o being Element of X such that

A23: o in M and

A24: o in N ;

reconsider o9 = o as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

A25: now :: thesis: ( b2 <> b4 implies a3,a4 // b3,b4 )

assume A26:
b2 <> b4
; :: thesis: a3,a4 // b3,b4

end;A27: now :: thesis: ( b1 <> b3 implies a3,a4 // b3,b4 )

ex d39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) st

( o9 <> d39 & d39 in N9 ) by A21, AFF_1:20;

then consider d3 being Element of X such that

A28: d3 in N and

A29: d3 <> o ;

reconsider d39 = d3 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

consider e2 being Element of X such that

A30: a3,a2 _|_ d3,e2 and

A31: d3 <> e2 by ANALMETR:def 9;

consider e1 being Element of X such that

A32: a3,a1 // a3,e1 and

A33: a3 <> e1 by ANALMETR:39;

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

assume A34: b1 <> b3 ; :: thesis: a3,a4 // b3,b4

A35: ( a1 <> a3 & a2 <> a4 )

A37: LIN a39,e19,d29 and

A38: LIN d39,e29,d29 by AFF_1:60;

reconsider d2 = d29 as Element of X ;

LIN d3,e2,d2 by A38, ANALMETR:40;

then d3,e2 // d3,d2 by ANALMETR:def 10;

then A39: a3,a2 _|_ d3,d2 by A30, A31, ANALMETR:62;

LIN a3,e1,d2 by A37, ANALMETR:40;

then a3,e1 // a3,d2 by ANALMETR:def 10;

then a3,a1 // a3,d2 by A32, A33, ANALMETR:60;

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

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

then consider d2 being Element of X such that

A40: d2 in M and

A41: a3,a2 _|_ d3,d2 by A3, A4, A22, A35, A39, AFF_1:25;

reconsider d29 = d2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

consider e1 being Element of X such that

A42: a2,a4 // a2,e1 and

A43: a2 <> e1 by ANALMETR:39;

consider e2 being Element of X such that

A44: a2,a1 _|_ d2,e2 and

A45: d2 <> e2 by ANALMETR:def 9;

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

not a29,e19 // d29,e29

A47: LIN a29,e19,d19 and

A48: LIN d29,e29,d19 by AFF_1:60;

reconsider d1 = d19 as Element of X ;

A49: b3,b2 _|_ d3,d2 by A4, A12, A18, A41, ANALMETR:62;

LIN a2,e1,d1 by A47, ANALMETR:40;

then a2,e1 // a2,d1 by ANALMETR:def 10;

then a2,a4 // a2,d1 by A42, A43, ANALMETR:60;

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

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

then A50: d1 in N by A7, A8, A21, A35, AFF_1:25;

LIN d2,e2,d1 by A48, ANALMETR:40;

then d2,e2 // d2,d1 by ANALMETR:def 10;

then A51: a2,a1 _|_ d2,d1 by A44, A45, ANALMETR:62;

then A52: b2,b1 _|_ d2,d1 by A3, A12, A19, ANALMETR:62;

consider e2 being Element of X such that

A53: a1,a4 _|_ d1,e2 and

A54: d1 <> e2 by ANALMETR:39;

consider e1 being Element of X such that

A55: a1,a3 // a1,e1 and

A56: a1 <> e1 by ANALMETR:39;

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

not a19,e19 // d19,e29

A58: LIN a19,e19,d49 and

A59: LIN d19,e29,d49 by AFF_1:60;

reconsider d4 = d49 as Element of X ;

LIN a1,e1,d4 by A58, ANALMETR:40;

then a1,e1 // a1,d4 by ANALMETR:def 10;

then a1,a3 // a1,d4 by A55, A56, ANALMETR:60;

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

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

then A60: d4 in M by A3, A4, A22, A35, AFF_1:25;

then A61: d3 <> d4 by A2, A22, A21, A23, A24, A28, A29, AFF_1:18;

LIN d1,e2,d4 by A59, ANALMETR:40;

then d1,e2 // d1,d4 by ANALMETR:def 10;

then A62: a1,a4 _|_ d1,d4 by A53, A54, ANALMETR:62;

then b1,b4 _|_ d1,d4 by A3, A11, A20, ANALMETR:62;

then A63: b3,b4 _|_ d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A28, A40, A50, A60, A49, A52;

a3,a4 _|_ d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A28, A40, A41, A50, A51, A60, A62;

hence a3,a4 // b3,b4 by A63, A61, ANALMETR:63; :: thesis: verum

end;( o9 <> d39 & d39 in N9 ) by A21, AFF_1:20;

then consider d3 being Element of X such that

A28: d3 in N and

A29: d3 <> o ;

reconsider d39 = d3 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

consider e2 being Element of X such that

A30: a3,a2 _|_ d3,e2 and

A31: d3 <> e2 by ANALMETR:def 9;

consider e1 being Element of X such that

A32: a3,a1 // a3,e1 and

A33: a3 <> e1 by ANALMETR:39;

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

assume A34: b1 <> b3 ; :: thesis: a3,a4 // b3,b4

A35: ( a1 <> a3 & a2 <> a4 )

proof

not a39,e19 // d39,e29
assume
( a1 = a3 or a2 = a4 )
; :: thesis: contradiction

then ( a2,a1 // b3,b2 or a1,a4 // b2,b1 ) by A18, A19, ANALMETR:59;

then ( b3,b2 // b2,b1 or b2,b1 // b1,b4 ) by A3, A11, A12, A19, A20, ANALMETR:60;

then ( b2,b3 // b2,b1 or b1,b2 // b1,b4 ) by ANALMETR:59;

then ( LIN b2,b3,b1 or LIN b1,b2,b4 ) by ANALMETR:def 10;

then ( LIN b29,b39,b19 or LIN b19,b29,b49 ) by ANALMETR:40;

then ( LIN b19,b39,b29 or LIN b29,b49,b19 ) by AFF_1:6;

hence contradiction by A5, A6, A9, A10, A13, A17, A22, A21, A26, A34, AFF_1:25; :: thesis: verum

end;then ( a2,a1 // b3,b2 or a1,a4 // b2,b1 ) by A18, A19, ANALMETR:59;

then ( b3,b2 // b2,b1 or b2,b1 // b1,b4 ) by A3, A11, A12, A19, A20, ANALMETR:60;

then ( b2,b3 // b2,b1 or b1,b2 // b1,b4 ) by ANALMETR:59;

then ( LIN b2,b3,b1 or LIN b1,b2,b4 ) by ANALMETR:def 10;

then ( LIN b29,b39,b19 or LIN b19,b29,b49 ) by ANALMETR:40;

then ( LIN b19,b39,b29 or LIN b29,b49,b19 ) by AFF_1:6;

hence contradiction by A5, A6, A9, A10, A13, A17, A22, A21, A26, A34, AFF_1:25; :: thesis: verum

proof

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

then a3,e1 // d3,e2 by ANALMETR:36;

then a3,a1 // d3,e2 by A32, A33, ANALMETR:60;

then A36: a3,a2 _|_ a3,a1 by A30, A31, ANALMETR:62;

a3,a1 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;

then a3,a2 // a2,a4 by A35, A36, ANALMETR:63;

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

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

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

hence contradiction by A7, A8, A16, A21, A35, AFF_1:25; :: thesis: verum

end;then a3,e1 // d3,e2 by ANALMETR:36;

then a3,a1 // d3,e2 by A32, A33, ANALMETR:60;

then A36: a3,a2 _|_ a3,a1 by A30, A31, ANALMETR:62;

a3,a1 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;

then a3,a2 // a2,a4 by A35, A36, ANALMETR:63;

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

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

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

hence contradiction by A7, A8, A16, A21, A35, AFF_1:25; :: thesis: verum

A37: LIN a39,e19,d29 and

A38: LIN d39,e29,d29 by AFF_1:60;

reconsider d2 = d29 as Element of X ;

LIN d3,e2,d2 by A38, ANALMETR:40;

then d3,e2 // d3,d2 by ANALMETR:def 10;

then A39: a3,a2 _|_ d3,d2 by A30, A31, ANALMETR:62;

LIN a3,e1,d2 by A37, ANALMETR:40;

then a3,e1 // a3,d2 by ANALMETR:def 10;

then a3,a1 // a3,d2 by A32, A33, ANALMETR:60;

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

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

then consider d2 being Element of X such that

A40: d2 in M and

A41: a3,a2 _|_ d3,d2 by A3, A4, A22, A35, A39, AFF_1:25;

reconsider d29 = d2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

consider e1 being Element of X such that

A42: a2,a4 // a2,e1 and

A43: a2 <> e1 by ANALMETR:39;

consider e2 being Element of X such that

A44: a2,a1 _|_ d2,e2 and

A45: d2 <> e2 by ANALMETR:def 9;

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

not a29,e19 // d29,e29

proof

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

then a2,e1 // d2,e2 by ANALMETR:36;

then a2,a4 // d2,e2 by A42, A43, ANALMETR:60;

then A46: a2,a4 _|_ a2,a1 by A44, A45, ANALMETR:62;

a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;

then a1,a3 // a2,a1 by A35, A46, ANALMETR:63;

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

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

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

hence contradiction by A3, A4, A12, A22, A35, AFF_1:25; :: thesis: verum

end;then a2,e1 // d2,e2 by ANALMETR:36;

then a2,a4 // d2,e2 by A42, A43, ANALMETR:60;

then A46: a2,a4 _|_ a2,a1 by A44, A45, ANALMETR:62;

a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;

then a1,a3 // a2,a1 by A35, A46, ANALMETR:63;

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

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

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

hence contradiction by A3, A4, A12, A22, A35, AFF_1:25; :: thesis: verum

A47: LIN a29,e19,d19 and

A48: LIN d29,e29,d19 by AFF_1:60;

reconsider d1 = d19 as Element of X ;

A49: b3,b2 _|_ d3,d2 by A4, A12, A18, A41, ANALMETR:62;

LIN a2,e1,d1 by A47, ANALMETR:40;

then a2,e1 // a2,d1 by ANALMETR:def 10;

then a2,a4 // a2,d1 by A42, A43, ANALMETR:60;

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

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

then A50: d1 in N by A7, A8, A21, A35, AFF_1:25;

LIN d2,e2,d1 by A48, ANALMETR:40;

then d2,e2 // d2,d1 by ANALMETR:def 10;

then A51: a2,a1 _|_ d2,d1 by A44, A45, ANALMETR:62;

then A52: b2,b1 _|_ d2,d1 by A3, A12, A19, ANALMETR:62;

consider e2 being Element of X such that

A53: a1,a4 _|_ d1,e2 and

A54: d1 <> e2 by ANALMETR:39;

consider e1 being Element of X such that

A55: a1,a3 // a1,e1 and

A56: a1 <> e1 by ANALMETR:39;

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

not a19,e19 // d19,e29

proof

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

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

then a1,a3 // d1,e2 by A55, A56, ANALMETR:60;

then A57: a1,a3 _|_ a1,a4 by A53, A54, ANALMETR:62;

a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;

then a2,a4 // a1,a4 by A35, A57, ANALMETR:63;

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

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

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

hence contradiction by A7, A8, A15, A21, A35, AFF_1:25; :: thesis: verum

end;then a1,e1 // d1,e2 by ANALMETR:36;

then a1,a3 // d1,e2 by A55, A56, ANALMETR:60;

then A57: a1,a3 _|_ a1,a4 by A53, A54, ANALMETR:62;

a1,a3 _|_ a2,a4 by A2, A3, A4, A7, A8, ANALMETR:56;

then a2,a4 // a1,a4 by A35, A57, ANALMETR:63;

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

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

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

hence contradiction by A7, A8, A15, A21, A35, AFF_1:25; :: thesis: verum

A58: LIN a19,e19,d49 and

A59: LIN d19,e29,d49 by AFF_1:60;

reconsider d4 = d49 as Element of X ;

LIN a1,e1,d4 by A58, ANALMETR:40;

then a1,e1 // a1,d4 by ANALMETR:def 10;

then a1,a3 // a1,d4 by A55, A56, ANALMETR:60;

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

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

then A60: d4 in M by A3, A4, A22, A35, AFF_1:25;

then A61: d3 <> d4 by A2, A22, A21, A23, A24, A28, A29, AFF_1:18;

LIN d1,e2,d4 by A59, ANALMETR:40;

then d1,e2 // d1,d4 by ANALMETR:def 10;

then A62: a1,a4 _|_ d1,d4 by A53, A54, ANALMETR:62;

then b1,b4 _|_ d1,d4 by A3, A11, A20, ANALMETR:62;

then A63: b3,b4 _|_ d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A28, A40, A50, A60, A49, A52;

a3,a4 _|_ d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A28, A40, A41, A50, A51, A60, A62;

hence a3,a4 // b3,b4 by A63, A61, ANALMETR:63; :: thesis: verum

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

hence
a3,a4 // b3,b4
by A27; :: thesis: verum
o9,a19 // o9,a39
by A3, A4, A22, A23, AFF_1:39, AFF_1:41;

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

assume A65: b1 = b3 ; :: thesis: a3,a4 // b3,b4

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

then a2,a1 // a3,a2 by A6, A13, A18, ANALMETR:60;

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

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

hence a3,a4 // b3,b4 by A7, A12, A15, A20, A21, A23, A24, A65, A64, AFF_1:14, AFF_1:25; :: thesis: verum

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

assume A65: b1 = b3 ; :: thesis: a3,a4 // b3,b4

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

then a2,a1 // a3,a2 by A6, A13, A18, ANALMETR:60;

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

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

hence a3,a4 // b3,b4 by A7, A12, A15, A20, A21, A23, A24, A65, A64, AFF_1:14, AFF_1:25; :: thesis: verum

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

hence
a3,a4 // b3,b4
by A25; :: thesis: verum
o9,a29 // o9,a49
by A7, A8, A21, A24, AFF_1:39, AFF_1:41;

then A66: LIN o9,a29,a49 by AFF_1:def 1;

assume A67: b2 = b4 ; :: thesis: a3,a4 // b3,b4

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

then a2,a1 // a1,a4 by A5, A13, A19, ANALMETR:60;

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

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

hence a3,a4 // b3,b4 by A3, A12, A15, A18, A22, A23, A24, A67, A66, AFF_1:14, AFF_1:25; :: thesis: verum

end;then A66: LIN o9,a29,a49 by AFF_1:def 1;

assume A67: b2 = b4 ; :: thesis: a3,a4 // b3,b4

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

then a2,a1 // a1,a4 by A5, A13, A19, ANALMETR:60;

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

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

hence a3,a4 // b3,b4 by A3, A12, A15, A18, A22, A23, A24, A67, A66, AFF_1:14, AFF_1:25; :: thesis: verum