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

assume A1: X is satisfying_MH1 ; :: 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_MH1 ; :: 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 )

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

A28: o9 <> e19 and

A29: e19 in M9 by A22, AFF_1:20;

reconsider e1 = e19 as Element of X ;

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

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

then consider d4 being Element of X such that

A30: d4 in N and

A31: d4 <> o ;

reconsider d49 = d4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

consider e2 being Element of X such that

A32: a1,a4 _|_ d4,e2 and

A33: e2 <> d4 by ANALMETR:39;

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

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

not o9,e19 // d49,e29

A39: LIN o9,e19,d19 and

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

reconsider d1 = d19 as Element of X ;

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

A41: o9 <> e19 and

A42: e19 in N9 by A21, AFF_1:20;

A43: d1 in M by A22, A23, A28, A29, A39, AFF_1:25;

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

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

then A44: d1,d4 // d4,e2 by ANALMETR:59;

then a1,a4 _|_ d1,d4 by A32, A33, ANALMETR:62;

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

reconsider e1 = e19 as Element of X ;

consider e2 being Element of X such that

A46: a2,a1 _|_ d1,e2 and

A47: e2 <> d1 by ANALMETR:39;

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

not o9,e19 // e29,d19

A53: LIN o9,e19,d29 and

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

reconsider d2 = d29 as Element of X ;

A55: d2 in N by A21, A24, A41, A42, A53, AFF_1:25;

LIN d19,d29,e29 by A54, AFF_1:6;

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

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

then A56: d2,d1 // e2,d1 by ANALMETR:59;

A57: a2,a1 _|_ e2,d1 by A46, ANALMETR:61;

then A58: a2,a1 _|_ d2,d1 by A47, A56, ANALMETR:62;

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

A59: o9 <> e19 and

A60: e19 in M9 by A22, AFF_1:20;

reconsider e1 = e19 as Element of X ;

consider e2 being Element of X such that

A61: a3,a2 _|_ d2,e2 and

A62: e2 <> d2 by ANALMETR:39;

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

not o9,e19 // e29,d29

A65: LIN o9,e19,d39 and

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

reconsider d3 = d39 as Element of X ;

A67: d3 in M by A22, A23, A59, A60, A65, AFF_1:25;

then A68: d3 <> d4 by A2, A22, A21, A23, A24, A30, A31, AFF_1:18;

a2,a1 _|_ d2,d1 by A47, A56, A57, ANALMETR:62;

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

LIN d29,d39,e29 by A66, AFF_1:6;

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

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

then d3,d2 // d2,e2 by ANALMETR:59;

then A70: a3,a2 _|_ d3,d2 by A61, A62, ANALMETR:62;

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

then A71: b3,b4 _|_ d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A30, A43, A55, A67, A45, A69;

a1,a4 _|_ d1,d4 by A32, A33, A44, ANALMETR:62;

then a3,a4 _|_ d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A30, A43, A55, A58, A70, A67;

hence a3,a4 // b3,b4 by A68, A71, ANALMETR:63; :: thesis: verum

end;A28: o9 <> e19 and

A29: e19 in M9 by A22, AFF_1:20;

reconsider e1 = e19 as Element of X ;

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

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

then consider d4 being Element of X such that

A30: d4 in N and

A31: d4 <> o ;

reconsider d49 = d4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;

consider e2 being Element of X such that

A32: a1,a4 _|_ d4,e2 and

A33: e2 <> d4 by ANALMETR:39;

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

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

not o9,e19 // d49,e29

proof

then consider d19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A35:
a49 <> a29

then o,e1 // d4,e2 by ANALMETR:36;

then A37: o,e1 _|_ a1,a4 by A32, A33, ANALMETR:62;

o9,e19 // a19,a39 by A3, A4, A22, A23, A29, AFF_1:39, AFF_1:41;

then o,e1 // a1,a3 by ANALMETR:36;

then A38: a1,a3 _|_ a1,a4 by A28, A37, ANALMETR:62;

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

then a1,a4 // a2,a4 by A38, A36, 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;proof

A36:
a1 <> a3
assume
a49 = a29
; :: thesis: contradiction

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

then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;

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

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

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

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

hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum

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

then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;

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

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

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

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

hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum

proof

assume
o9,e19 // d49,e29
; :: thesis: contradiction
assume
a1 = a3
; :: thesis: contradiction

then a3,a2 // b2,b1 by A19, ANALMETR:59;

then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;

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

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

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

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

hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; :: thesis: verum

end;then a3,a2 // b2,b1 by A19, ANALMETR:59;

then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;

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

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

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

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

hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; :: thesis: verum

then o,e1 // d4,e2 by ANALMETR:36;

then A37: o,e1 _|_ a1,a4 by A32, A33, ANALMETR:62;

o9,e19 // a19,a39 by A3, A4, A22, A23, A29, AFF_1:39, AFF_1:41;

then o,e1 // a1,a3 by ANALMETR:36;

then A38: a1,a3 _|_ a1,a4 by A28, A37, ANALMETR:62;

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

then a1,a4 // a2,a4 by A38, A36, 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

A39: LIN o9,e19,d19 and

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

reconsider d1 = d19 as Element of X ;

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

A41: o9 <> e19 and

A42: e19 in N9 by A21, AFF_1:20;

A43: d1 in M by A22, A23, A28, A29, A39, AFF_1:25;

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

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

then A44: d1,d4 // d4,e2 by ANALMETR:59;

then a1,a4 _|_ d1,d4 by A32, A33, ANALMETR:62;

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

reconsider e1 = e19 as Element of X ;

consider e2 being Element of X such that

A46: a2,a1 _|_ d1,e2 and

A47: e2 <> d1 by ANALMETR:39;

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

not o9,e19 // e29,d19

proof

then consider d29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A48:
a19 <> a39

then A49: o,e1 // a2,a4 by ANALMETR:36;

A50: a2 <> a4

then A51: o,e1 // e2,d1 by ANALMETR:36;

a2,a1 _|_ e2,d1 by A46, ANALMETR:61;

then o,e1 _|_ a2,a1 by A47, A51, ANALMETR:62;

then A52: a2,a1 _|_ a2,a4 by A41, A49, ANALMETR:62;

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

then a3,a1 // a2,a1 by A52, A50, 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, A48, AFF_1:25; :: thesis: verum

end;proof

o9,e19 // a29,a49
by A7, A8, A21, A24, A42, AFF_1:39, AFF_1:41;
assume
a19 = a39
; :: thesis: contradiction

then a3,a2 // b2,b1 by A19, ANALMETR:59;

then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;

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

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

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

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

hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; :: thesis: verum

end;then a3,a2 // b2,b1 by A19, ANALMETR:59;

then b3,b2 // b2,b1 by A4, A12, A18, ANALMETR:60;

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

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

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

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

hence contradiction by A5, A6, A13, A22, A34, AFF_1:25; :: thesis: verum

then A49: o,e1 // a2,a4 by ANALMETR:36;

A50: a2 <> a4

proof

assume
o9,e19 // e29,d19
; :: thesis: contradiction
assume
a2 = a4
; :: thesis: contradiction

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

then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;

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

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

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

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

hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum

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

then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;

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

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

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

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

hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum

then A51: o,e1 // e2,d1 by ANALMETR:36;

a2,a1 _|_ e2,d1 by A46, ANALMETR:61;

then o,e1 _|_ a2,a1 by A47, A51, ANALMETR:62;

then A52: a2,a1 _|_ a2,a4 by A41, A49, ANALMETR:62;

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

then a3,a1 // a2,a1 by A52, A50, 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, A48, AFF_1:25; :: thesis: verum

A53: LIN o9,e19,d29 and

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

reconsider d2 = d29 as Element of X ;

A55: d2 in N by A21, A24, A41, A42, A53, AFF_1:25;

LIN d19,d29,e29 by A54, AFF_1:6;

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

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

then A56: d2,d1 // e2,d1 by ANALMETR:59;

A57: a2,a1 _|_ e2,d1 by A46, ANALMETR:61;

then A58: a2,a1 _|_ d2,d1 by A47, A56, ANALMETR:62;

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

A59: o9 <> e19 and

A60: e19 in M9 by A22, AFF_1:20;

reconsider e1 = e19 as Element of X ;

consider e2 being Element of X such that

A61: a3,a2 _|_ d2,e2 and

A62: e2 <> d2 by ANALMETR:39;

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

not o9,e19 // e29,d29

proof

then consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A63:
a29 <> a49

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

then o,e1 // d2,e2 by ANALMETR:59;

then A64: a3,a2 _|_ o,e1 by A61, A62, ANALMETR:62;

o,e1 _|_ a2,a4 by A2, A7, A8, A23, A60, ANALMETR:56;

then a3,a2 // a2,a4 by A59, A64, 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, A63, AFF_1:25; :: thesis: verum

end;proof

assume
o9,e19 // e29,d29
; :: thesis: contradiction
assume
a29 = a49
; :: thesis: contradiction

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

then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;

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

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

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

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

hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum

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

then b1,b4 // b2,b1 by A3, A12, A19, ANALMETR:60;

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

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

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

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

hence contradiction by A9, A10, A17, A21, A26, AFF_1:25; :: thesis: verum

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

then o,e1 // d2,e2 by ANALMETR:59;

then A64: a3,a2 _|_ o,e1 by A61, A62, ANALMETR:62;

o,e1 _|_ a2,a4 by A2, A7, A8, A23, A60, ANALMETR:56;

then a3,a2 // a2,a4 by A59, A64, 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, A63, AFF_1:25; :: thesis: verum

A65: LIN o9,e19,d39 and

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

reconsider d3 = d39 as Element of X ;

A67: d3 in M by A22, A23, A59, A60, A65, AFF_1:25;

then A68: d3 <> d4 by A2, A22, A21, A23, A24, A30, A31, AFF_1:18;

a2,a1 _|_ d2,d1 by A47, A56, A57, ANALMETR:62;

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

LIN d29,d39,e29 by A66, AFF_1:6;

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

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

then d3,d2 // d2,e2 by ANALMETR:59;

then A70: a3,a2 _|_ d3,d2 by A61, A62, ANALMETR:62;

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

then A71: b3,b4 _|_ d3,d4 by A1, A2, A5, A6, A9, A10, A13, A14, A30, A43, A55, A67, A45, A69;

a1,a4 _|_ d1,d4 by A32, A33, A44, ANALMETR:62;

then a3,a4 _|_ d3,d4 by A1, A2, A3, A4, A7, A8, A11, A12, A30, A43, A55, A58, A70, A67;

hence a3,a4 // b3,b4 by A68, A71, ANALMETR:63; :: thesis: verum

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

hence
a3,a4 // b3,b4
by A27; :: thesis: verumA72:
not LIN o9,a29,a19
by A7, A12, A15, A21, A23, A24, AFF_1:48, AFF_1:def 1;

A73: LIN o9,a19,a39 by A3, A4, A22, A23, AFF_1:21;

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

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

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

a29,a19 // b29,b19 by A19, ANALMETR:36;

then a29,a19 // a29,a39 by A5, A13, A75, AFF_1:5;

hence a3,a4 // b3,b4 by A20, A74, A72, A73, AFF_1:14; :: thesis: verum

end;A73: LIN o9,a19,a39 by A3, A4, A22, A23, AFF_1:21;

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

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

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

a29,a19 // b29,b19 by A19, ANALMETR:36;

then a29,a19 // a29,a39 by A5, A13, A75, AFF_1:5;

hence a3,a4 // b3,b4 by A20, A74, A72, A73, AFF_1:14; :: thesis: verum

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

hence
a3,a4 // b3,b4
by A25; :: thesis: verumA76:
not LIN o9,a19,a49

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

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

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

LIN o9,a49,a29 by A7, A8, A21, A24, AFF_1:21;

hence a3,a4 // b3,b4 by A18, A77, A78, A76, AFF_1:14; :: thesis: verum

end;proof

assume A77:
b2 = b4
; :: thesis: a3,a4 // b3,b4
assume
LIN o9,a19,a49
; :: thesis: contradiction

then ex A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) st

( A9 is being_line & o9 in A9 & a19 in A9 & a49 in A9 ) by AFF_1:21;

hence contradiction by A3, A11, A15, A22, A23, A24, AFF_1:18; :: thesis: verum

end;then ex A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) st

( A9 is being_line & o9 in A9 & a19 in A9 & a49 in A9 ) by AFF_1:21;

hence contradiction by A3, A11, A15, A22, A23, A24, AFF_1:18; :: thesis: verum

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

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

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

LIN o9,a49,a29 by A7, A8, A21, A24, AFF_1:21;

hence a3,a4 // b3,b4 by A18, A77, A78, A76, AFF_1:14; :: thesis: verum