let X be OrtAfPl; :: thesis: ( X is satisfying_MH1 & X is satisfying_MH2 implies X is satisfying_OPAP )
assume A1: X is satisfying_MH1 ; :: thesis: ( not X is satisfying_MH2 or X is satisfying_OPAP )
assume A2: X is satisfying_MH2 ; :: 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
A3: o in M and
A4: a1 in M and
A5: a2 in M and
A6: a3 in M and
A7: o in N and
A8: b1 in N and
A9: b2 in N and
A10: b3 in N and
A11: not b2 in M and
A12: not a3 in N and
A13: M _|_ N and
A14: o <> a1 and
A15: o <> a2 and
o <> a3 and
A16: o <> b1 and
o <> b2 and
A17: o <> b3 and
A18: a3,b2 // a2,b1 and
A19: 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 A13, ANALMETR:44;
then A20: N9 is being_line by ANALMETR:43;
M is being_line by A13, ANALMETR:44;
then A21: M9 is being_line by ANALMETR:43;

A22: now :: thesis: ( a1 <> a2 & a2 <> a3 & a1 <> a3 implies ex d4 being Element of X st a1,b2 // a2,b3 )

consider e1 being Element of X such that
A23: o,a3 // o,e1 and
A24: o <> e1 by ANALMETR:39;
consider d1 being Element of X such that
A25: o,b3 // o,d1 and
A26: o <> d1 by ANALMETR:39;
reconsider d19 = d1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
consider e2 being Element of X such that
A27: a1,b3 _|_ d1,e2 and
A28: d1 <> e2 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
assume that
A29: a1 <> a2 and
a2 <> a3 and
A30: a1 <> a3 ; :: thesis: ex d4 being Element of X st a1,b2 // a2,b3
A31: LIN o,b3,d1 by A25, ANALMETR:def 10;
then A32: LIN o9,b39,d19 by ANALMETR:40;
N is being_line by A13, ANALMETR:44;
then A33: N9 is being_line by ANALMETR:43;
then A34: o9,b29 // o9,b39 by A7, A9, A10, AFF_1:39, AFF_1:41;
then o,b2 // o,b3 by ANALMETR:36;
then A35: LIN o,b2,b3 by ANALMETR:def 10;
A36: b2 <> b3

proof

A37: not LIN o9,b19,a29

proof

o9,a29 // o9,a39 by A3, A5, A6, A21, AFF_1:39, AFF_1:41;
then A38: LIN o9,a29,a39 by AFF_1:def 1;
assume LIN o9,b19,a29 ; :: thesis: contradiction
then a29 in N9 by A7, A8, A16, A20, AFF_1:25;
hence contradiction by A7, A12, A15, A20, A38, AFF_1:25; :: thesis: verum

end;

assume b2 = b3 ; :: thesis: contradiction
then a1,b1 // a2,b1 by A6, A11, A18, A19, ANALMETR:60;
then b1,a2 // b1,a1 by ANALMETR:59;
then A39: b19,a29 // b19,a19 by ANALMETR:36;
o9,a29 // o9,a19 by A3, A4, A5, A21, AFF_1:39, AFF_1:41;
then LIN o9,a29,a19 by AFF_1:def 1;
hence contradiction by A29, A37, A39, AFF_1:14; :: thesis: verum

end;

A40: not LIN b2,a3,b3

proof

assume LIN b2,a3,b3 ; :: thesis: contradiction
then LIN b29,a39,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A9, A10, A12, A36, A33, AFF_1:25; :: thesis: verum

end;

A41: a3 <> b3

proof

assume a3 = b3 ; :: thesis: contradiction
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

b29,b39 // b29,b19 by A8, A9, A10, A33, AFF_1:39, AFF_1:41;
then b2,b3 // b2,b1 by ANALMETR:36;
then A42: LIN b2,b3,b1 by ANALMETR:def 10;
M is being_line by A13, ANALMETR:44;
then A43: M9 is being_line by ANALMETR:43;
then o9,a39 // o9,a19 by A3, A4, A6, AFF_1:39, AFF_1:41;
then A44: o,a3 // o,a1 by ANALMETR:36;
then A45: LIN o,a3,a1 by ANALMETR:def 10;
A46: not LIN a3,a1,b2

proof

assume LIN a3,a1,b2 ; :: thesis: contradiction
then LIN a39,a19,b29 by ANALMETR:40;
hence contradiction by A4, A6, A11, A30, A43, AFF_1:25; :: thesis: verum

end;

A47: a3 <> b2

proof

assume a3 = b2 ; :: thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

A48: o,a3 _|_ o,b3 by A3, A6, A7, A10, A13, ANALMETR:56;
not o,e1 // d1,e2

proof

reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
assume o,e1 // d1,e2 ; :: thesis: contradiction
then o9,e19 // d19,e29 by ANALMETR:36;
then d19,e29 // o9,e19 by AFF_1:4;
then d1,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ a1,b3 by A27, A28, ANALMETR:62;
then o,a3 _|_ a1,b3 by A23, A24, ANALMETR:62;
then o,b3 // a1,b3 by A7, A12, A48, ANALMETR:63;
then o9,b39 // a19,b39 by ANALMETR:36;
then b39,o9 // b39,a19 by AFF_1:4;
then LIN b39,o9,a19 by AFF_1:def 1;
then LIN o9,b39,a19 by AFF_1:6;
then A49: o9,b39 // o9,a19 by AFF_1:def 1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then o9,b29 // o9,b39 by AFF_1:def 1;
then o9,b39 // o9,b29 by AFF_1:4;
then o9,a19 // o9,b29 by A17, A49, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then A50: a19,o9 // a19,b29 by AFF_1:def 1;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a19,b29 // a19,a39 by A14, A50, DIRAF:40;
then LIN a19,b29,a39 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

then not o9,e19 // d19,e29 by ANALMETR:36;
then consider d29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A51: LIN o9,e19,d29 and
A52: LIN d19,e29,d29 by AFF_1:60;
reconsider d2 = d29 as Element of X ;
LIN d1,e2,d2 by A52, ANALMETR:40;
then A53: d1,e2 // d1,d2 by ANALMETR:def 10;
then A54: a1,b3 _|_ d1,d2 by A27, A28, ANALMETR:62;
then A55: d1,d2 _|_ b3,a1 by ANALMETR:61;
LIN o,e1,d2 by A51, ANALMETR:40;
then o,e1 // o,d2 by ANALMETR:def 10;
then A56: o,a3 // o,d2 by A23, A24, ANALMETR:60;
then A57: LIN o,a3,d2 by ANALMETR:def 10;
then A58: LIN o9,a39,d29 by ANALMETR:40;
consider e1 being Element of X such that
A59: o,b3 // o,e1 and
A60: o <> e1 by ANALMETR:39;
consider e2 being Element of X such that
A61: b3,a3 _|_ d2,e2 and
A62: d2 <> e2 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
not o,e1 // d2,e2

proof

reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
assume o,e1 // d2,e2 ; :: thesis: contradiction
then o9,e19 // d29,e29 by ANALMETR:36;
then d29,e29 // o9,e19 by AFF_1:4;
then d2,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ b3,a3 by A61, A62, ANALMETR:62;
then o,b3 _|_ b3,a3 by A59, A60, ANALMETR:62;
then b3,a3 // o,a3 by A17, A48, ANALMETR:63;
then b39,a39 // o9,a39 by ANALMETR:36;
then a39,b39 // a39,o9 by AFF_1:4;
then LIN a39,b39,o9 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then A63: b39,o9 // b39,a39 by AFF_1:def 1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b39,a39 // b39,b29 by A17, A63, DIRAF:40;
then LIN b39,a39,b29 by AFF_1:def 1;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

then not o9,e19 // d29,e29 by ANALMETR:36;
then consider d39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A64: LIN o9,e19,d39 and
A65: LIN d29,e29,d39 by AFF_1:60;
reconsider d3 = d39 as Element of X ;
LIN d2,e2,d3 by A65, ANALMETR:40;
then A66: d2,e2 // d2,d3 by ANALMETR:def 10;
then A67: b3,a3 _|_ d2,d3 by A61, A62, ANALMETR:62;
then d2,d3 _|_ a3,b3 by ANALMETR:61;
then A68: d2,d3 _|_ a1,b1 by A19, A41, ANALMETR:62;
LIN o,e1,d3 by A64, ANALMETR:40;
then o,e1 // o,d3 by ANALMETR:def 10;
then A69: o,b3 // o,d3 by A59, A60, ANALMETR:60;
then A70: LIN o,b3,d3 by ANALMETR:def 10;
then A71: LIN o9,b39,d39 by ANALMETR:40;
consider e2 being Element of X such that
A72: a3,b2 _|_ d3,e2 and
A73: d3 <> e2 by ANALMETR:39;
consider e1 being Element of X such that
A74: o,a3 // o,e1 and
A75: o <> e1 by ANALMETR:39;
reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
not o,e1 // d3,e2

proof

reconsider e19 = e1, e29 = e2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b29,o9,b39 by AFF_1:6;
then A76: b29,o9 // b29,b39 by AFF_1:def 1;
assume o,e1 // d3,e2 ; :: thesis: contradiction
then o9,e19 // d39,e29 by ANALMETR:36;
then d39,e29 // o9,e19 by AFF_1:4;
then d3,e2 // o,e1 by ANALMETR:36;
then o,e1 _|_ a3,b2 by A72, A73, ANALMETR:62;
then o,a3 _|_ a3,b2 by A74, A75, ANALMETR:62;
then A77: o,b3 // a3,b2 by A7, A12, A48, ANALMETR:63;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN o9,b39,b29 by AFF_1:6;
then LIN o,b3,b2 by ANALMETR:40;
then o,b3 // o,b2 by ANALMETR:def 10;
then o,b2 // a3,b2 by A17, A77, ANALMETR:60;
then o9,b29 // a39,b29 by ANALMETR:36;
then b29,o9 // b29,a39 by AFF_1:4;
then b29,a39 // b29,b39 by A3, A11, A76, DIRAF:40;
then LIN b29,a39,b39 by AFF_1:def 1;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

then not o9,e19 // d39,e29 by ANALMETR:36;
then consider d49 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A78: LIN o9,e19,d49 and
A79: LIN d39,e29,d49 by AFF_1:60;
reconsider d4 = d49 as Element of X ;
LIN d3,e2,d4 by A79, ANALMETR:40;
then A80: d3,e2 // d3,d4 by ANALMETR:def 10;
then A81: d3,d4 _|_ a3,b2 by A72, A73, ANALMETR:62;
LIN o,e1,d4 by A78, ANALMETR:40;
then o,e1 // o,d4 by ANALMETR:def 10;
then A82: o,a3 // o,d4 by A74, A75, ANALMETR:60;
then A83: LIN o,a3,d4 by ANALMETR:def 10;
then A84: LIN o9,a39,d49 by ANALMETR:40;
A85: a3,b2 _|_ d3,d4 by A72, A73, A80, ANALMETR:62;
then ( d3,d4 _|_ a2,b1 or a3 = b2 ) by A18, ANALMETR:62;
then A86: d3,d4 _|_ b1,a2 by A47, ANALMETR:61;
A87: d2 <> o

proof

o,a3 _|_ o,d1 by A17, A48, A25, ANALMETR:62;
then A88: d1,o _|_ o,a3 by ANALMETR:61;
assume d2 = o ; :: thesis: contradiction
then d1,o _|_ a1,b3 by A27, A28, A53, ANALMETR:62;
then o,a3 // a1,b3 by A26, A88, ANALMETR:63;
then a1,b3 // o,a1 by A7, A12, A44, ANALMETR:60;
then a19,b39 // o9,a19 by ANALMETR:36;
then a19,b39 // a19,o9 by AFF_1:4;
then LIN a19,b39,o9 by AFF_1:def 1;
then LIN o9,b39,a19 by AFF_1:6;
then A89: o9,b39 // o9,a19 by AFF_1:def 1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN o9,b39,b29 by AFF_1:6;
then o9,b39 // o9,b29 by AFF_1:def 1;
then o9,a19 // o9,b29 by A17, A89, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then A90: a19,o9 // a19,b29 by AFF_1:def 1;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a19,b29 // a19,a39 by A14, A90, DIRAF:40;
then LIN a19,b29,a39 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

A91: not LIN d1,d2,d3

proof

A92: d2 <> d3

proof

assume d2 = d3 ; :: thesis: contradiction
then o9,b39 // o9,d29 by A69, ANALMETR:36;
then o9,d29 // o9,b39 by AFF_1:4;
then o,d2 // o,b3 by ANALMETR:36;
then o,b3 // o,a3 by A56, A87, ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def 1;
then A93: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17, A93, ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

A94: d1 <> d2

proof

assume d1 = d2 ; :: thesis: contradiction
then o9,a39 // o9,d19 by A56, ANALMETR:36;
then o9,d19 // o9,a39 by AFF_1:4;
then o,d1 // o,a3 by ANALMETR:36;
then o,b3 // o,a3 by A25, A26, ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def 1;
then A95: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17, A95, ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

assume LIN d1,d2,d3 ; :: thesis: contradiction
then LIN d19,d29,d39 by ANALMETR:40;
then LIN d29,d19,d39 by AFF_1:6;
then d29,d19 // d29,d39 by AFF_1:def 1;
then d19,d29 // d29,d39 by AFF_1:4;
then d1,d2 // d2,d3 by ANALMETR:36;
then d2,d3 _|_ a1,b3 by A54, A94, ANALMETR:62;
then a1,b3 // b3,a3 by A67, A92, ANALMETR:63;
then a19,b39 // b39,a39 by ANALMETR:36;
then b39,a19 // b39,a39 by AFF_1:4;
then LIN b39,a19,a39 by AFF_1:def 1;
then LIN a19,a39,b39 by AFF_1:6;
then a19,a39 // a19,b39 by AFF_1:def 1;
then A96: a1,a3 // a1,b3 by ANALMETR:36;
A97: a1 <> a3

proof

assume a1 = a3 ; :: thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,a39,o9 by AFF_1:6;
then a19,a39 // a19,o9 by AFF_1:def 1;
then a1,a3 // a1,o by ANALMETR:36;
then a1,o // a1,b3 by A97, A96, ANALMETR:60;
then LIN a1,o,b3 by ANALMETR:def 10;
then LIN a19,o9,b39 by ANALMETR:40;
then LIN o9,b39,a19 by AFF_1:6;
then A98: o9,b39 // o9,a19 by AFF_1:def 1;
o9,b39 // o9,b29 by A34, AFF_1:4;
then o9,a19 // o9,b29 by A17, A98, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then a19,o9 // a19,b29 by AFF_1:def 1;
then A99: a1,o // a1,b2 by ANALMETR:36;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a1,o // a1,a3 by ANALMETR:36;
then a1,b2 // a1,a3 by A14, A99, ANALMETR:60;
then LIN a1,b2,a3 by ANALMETR:def 10;
then LIN a19,b29,a39 by ANALMETR:40;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

A100: d2 <> d4

proof

A101: d2 <> d3

proof

assume d2 = d3 ; :: thesis: contradiction
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91, ANALMETR:40; :: thesis: verum

end;

assume d2 = d4 ; :: thesis: contradiction
then a3,b2 _|_ d2,d3 by A85, ANALMETR:61;
then a3,b2 // b3,a3 by A67, A101, ANALMETR:63;
then a3,b2 // a3,b3 by ANALMETR:59;
then LIN a3,b2,b3 by ANALMETR:def 10;
then LIN a39,b29,b39 by ANALMETR:40;
then LIN b29,b39,a39 by AFF_1:6;
hence contradiction by A9, A10, A12, A20, A36, AFF_1:25; :: thesis: verum

end;

LIN o9,b39,b39 by AFF_1:7;
then A102: LIN d19,d39,b39 by A17, A32, A71, AFF_1:8;
then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A103: A9 is being_line and
A104: d19 in A9 and
A105: d39 in A9 and
A106: b39 in A9 by AFF_1:21;
reconsider A = A9 as Subset of X ;
A107: d19 <> d39

proof

assume d19 = d39 ; :: thesis: contradiction
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91, ANALMETR:40; :: thesis: verum

end;

then A9 = Line (d19,d39) by A103, A104, A105, AFF_1:24;
then A108: A = Line (d1,d3) by ANALMETR:41;
LIN o9,b29,b39 by A35, ANALMETR:40;
then A109: LIN o9,b39,b29 by AFF_1:6;
then A110: b2 in A by A17, A32, A71, A103, A104, A105, A107, AFF_1:8, AFF_1:25;
A111: o <> d3

proof

assume d3 = o ; :: thesis: contradiction
then A112: d2,o _|_ b3,a3 by A61, A62, A66, ANALMETR:62;
o,b3 _|_ o,d2 by A7, A12, A48, A56, ANALMETR:62;
then d2,o _|_ o,b3 by ANALMETR:61;
then o,b3 // b3,a3 by A87, A112, ANALMETR:63;
then o9,b39 // b39,a39 by ANALMETR:36;
then A113: b39,o9 // b39,a39 by AFF_1:4;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b39,a39 // b39,b29 by A17, A113, DIRAF:40;
then LIN b39,a39,b29 by AFF_1:def 1;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

A114: o <> d4

proof

o,a3 _|_ o,d3 by A17, A48, A69, ANALMETR:62;
then A115: d3,o _|_ o,a3 by ANALMETR:61;
assume d4 = o ; :: thesis: contradiction
then d3,o _|_ a3,b2 by A72, A73, A80, ANALMETR:62;
then o,a3 // a3,b2 by A111, A115, ANALMETR:63;
then o9,a39 // a39,b29 by ANALMETR:36;
then A116: a39,o9 // a39,b29 by AFF_1:4;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a39,o9,a19 by AFF_1:6;
then a39,o9 // a39,a19 by AFF_1:def 1;
then a39,b29 // a39,a19 by A7, A12, A116, DIRAF:40;
then LIN a39,b29,a19 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

A117: not LIN d1,d4,d3

proof

A118: d1 <> d3

proof

A119: d1 <> d2

proof

assume d1 = d2 ; :: thesis: contradiction
then o9,a39 // o9,d19 by A56, ANALMETR:36;
then o9,d19 // o9,a39 by AFF_1:4;
then o,d1 // o,a3 by ANALMETR:36;
then o,b3 // o,a3 by A25, A26, ANALMETR:60;
then o9,b39 // o9,a39 by ANALMETR:36;
then LIN o9,b39,a39 by AFF_1:def 1;
then LIN b39,o9,a39 by AFF_1:6;
then b39,o9 // b39,a39 by AFF_1:def 1;
then A120: b3,o // b3,a3 by ANALMETR:36;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,o9,b29 by AFF_1:6;
then b39,o9 // b39,b29 by AFF_1:def 1;
then b3,o // b3,b2 by ANALMETR:36;
then b3,b2 // b3,a3 by A17, A120, ANALMETR:60;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
then LIN b29,a39,b39 by AFF_1:6;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

assume d1 = d3 ; :: thesis: contradiction
then a3,b3 _|_ d1,d2 by A67, ANALMETR:61;
then a1,b3 // a3,b3 by A54, A119, ANALMETR:63;
then a19,b39 // a39,b39 by ANALMETR:36;
then b39,a19 // b39,a39 by AFF_1:4;
then LIN b39,a19,a39 by AFF_1:def 1;
then LIN a19,a39,b39 by AFF_1:6;
then a19,a39 // a19,b39 by AFF_1:def 1;
then A121: a1,a3 // a1,b3 by ANALMETR:36;
A122: a1 <> a3

proof

assume a1 = a3 ; :: thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,a39,o9 by AFF_1:6;
then a19,a39 // a19,o9 by AFF_1:def 1;
then a1,a3 // a1,o by ANALMETR:36;
then a1,o // a1,b3 by A122, A121, ANALMETR:60;
then LIN a1,o,b3 by ANALMETR:def 10;
then LIN a19,o9,b39 by ANALMETR:40;
then LIN o9,b39,a19 by AFF_1:6;
then A123: o9,b39 // o9,a19 by AFF_1:def 1;
o9,b39 // o9,b29 by A34, AFF_1:4;
then o9,a19 // o9,b29 by A17, A123, DIRAF:40;
then LIN o9,a19,b29 by AFF_1:def 1;
then LIN a19,o9,b29 by AFF_1:6;
then a19,o9 // a19,b29 by AFF_1:def 1;
then A124: a1,o // a1,b2 by ANALMETR:36;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a19,o9,a39 by AFF_1:6;
then a19,o9 // a19,a39 by AFF_1:def 1;
then a1,o // a1,a3 by ANALMETR:36;
then a1,b2 // a1,a3 by A14, A124, ANALMETR:60;
then LIN a1,b2,a3 by ANALMETR:def 10;
then LIN a19,b29,a39 by ANALMETR:40;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

assume LIN d1,d4,d3 ; :: thesis: contradiction
then LIN d19,d49,d39 by ANALMETR:40;
then A125: LIN d19,d39,d49 by AFF_1:6;
A126: b29 <> b39

proof

assume b29 = b39 ; :: thesis: contradiction
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b29,b39,o9 by AFF_1:6;
then A127: b29,b39 // b29,o9 by AFF_1:def 1;
LIN d19,d39,b29 by A17, A32, A71, A109, AFF_1:8;
then LIN b29,b39,d49 by A102, A118, A125, AFF_1:8;
then b29,b39 // b29,d49 by AFF_1:def 1;
then b29,o9 // b29,d49 by A127, A126, DIRAF:40;
then LIN b29,o9,d49 by AFF_1:def 1;
then LIN o9,d49,b29 by AFF_1:6;
then A128: o9,d49 // o9,b29 by AFF_1:def 1;
o9,a39 // o9,d49 by A82, ANALMETR:36;
then o9,d49 // o9,a39 by AFF_1:4;
then o9,b29 // o9,a39 by A114, A128, DIRAF:40;
then LIN o9,b29,a39 by AFF_1:def 1;
then LIN b29,o9,a39 by AFF_1:6;
then A129: b29,o9 // b29,a39 by AFF_1:def 1;
LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b29,o9,b39 by AFF_1:6;
then b29,o9 // b29,b39 by AFF_1:def 1;
then b29,a39 // b29,b39 by A3, A11, A129, DIRAF:40;
then LIN b29,a39,b39 by AFF_1:def 1;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

A130: not d4 in A

proof

assume d4 in A ; :: thesis: contradiction
then d19,d49 // d19,d39 by A103, A104, A105, AFF_1:39, AFF_1:41;
then LIN d19,d49,d39 by AFF_1:def 1;
hence contradiction by A117, ANALMETR:40; :: thesis: verum

end;

A131: d2,d3 _|_ b3,a3 by A61, A62, A66, ANALMETR:62;
take d4 = d4; :: thesis: a1,b2 // a2,b3
LIN o9,b39,d19 by A31, ANALMETR:40;
then A132: o9,b39 // o9,d19 by AFF_1:def 1;
LIN o9,a39,a19 by A45, ANALMETR:40;
then A133: LIN d29,d49,a19 by A7, A12, A58, A84, AFF_1:8;
then consider K9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A134: K9 is being_line and
A135: d29 in K9 and
A136: d49 in K9 and
A137: a19 in K9 by AFF_1:21;
reconsider K = K9 as Subset of X ;
LIN o9,a39,a39 by AFF_1:7;
then A138: a3 in K by A7, A12, A58, A84, A100, A134, A135, A136, AFF_1:8, AFF_1:25;
a39,a19 // a39,a29 by A4, A5, A6, A43, AFF_1:39, AFF_1:41;
then a3,a1 // a3,a2 by ANALMETR:36;
then A139: LIN a3,a1,a2 by ANALMETR:def 10;
A140: ( LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2 )

proof

A141: b39 <> b29

proof

assume b39 = b29 ; :: thesis: contradiction
then LIN b29,a39,b39 by AFF_1:7;
hence contradiction by A40, ANALMETR:40; :: thesis: verum

end;

LIN o9,b29,b39 by A35, ANALMETR:40;
then LIN b39,b29,o9 by AFF_1:6;
then A142: b39,b29 // b39,o9 by AFF_1:def 1;
LIN b29,b39,b19 by A42, ANALMETR:40;
then LIN b39,b29,b19 by AFF_1:6;
then b39,b29 // b39,b19 by AFF_1:def 1;
then b39,b19 // b39,o9 by A142, A141, DIRAF:40;
then LIN b39,b19,o9 by AFF_1:def 1;
then A143: LIN o9,b39,b19 by AFF_1:6;
A144: LIN o9,b39,d39 by A70, ANALMETR:40;
LIN o9,b39,d19 by A31, ANALMETR:40;
then A145: LIN d19,d39,b19 by A17, A143, A144, AFF_1:8;
reconsider o9 = o, a19 = a1, a29 = a2, a39 = a3, d29 = d2, d49 = d4 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
A146: a39 <> a19

proof

assume a19 = a39 ; :: thesis: contradiction
then LIN a39,a19,b29 by AFF_1:7;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a39,a19,o9 by AFF_1:6;
then A147: a39,a19 // a39,o9 by AFF_1:def 1;
LIN a39,a19,a29 by A139, ANALMETR:40;
then a39,a19 // a39,a29 by AFF_1:def 1;
then a39,a29 // a39,o9 by A147, A146, DIRAF:40;
then LIN a39,a29,o9 by AFF_1:def 1;
then A148: LIN o9,a39,a29 by AFF_1:6;
A149: LIN o9,a39,d49 by A83, ANALMETR:40;
LIN o9,a39,d29 by A57, ANALMETR:40;
then LIN d29,d49,a29 by A7, A12, A148, A149, AFF_1:8;
hence ( LIN d1,d3,b3 & LIN d1,d3,b1 & LIN d2,d4,a1 & LIN d2,d4,a2 ) by A102, A133, A145, ANALMETR:40; :: thesis: verum

end;

LIN o9,b39,d39 by A70, ANALMETR:40;
then o9,b39 // o9,d39 by AFF_1:def 1;
then o9,d19 // o9,d39 by A17, A132, DIRAF:40;
then LIN o9,d19,d39 by AFF_1:def 1;
then LIN d19,o9,d39 by AFF_1:6;
then d19,o9 // d19,d39 by AFF_1:def 1;
then o9,d19 // d19,d39 by AFF_1:4;
then A150: o,d1 // d1,d3 by ANALMETR:36;
o,b3 // o,d1 by A132, ANALMETR:36;
then o,d1 _|_ o,a3 by A17, A48, ANALMETR:62;
then A151: o,a3 _|_ d1,d3 by A26, A150, ANALMETR:62;
LIN o9,a39,d29 by A57, ANALMETR:40;
then A152: o9,a39 // o9,d29 by AFF_1:def 1;
then o,a3 // o,d2 by ANALMETR:36;
then A153: o,d2 _|_ d1,d3 by A7, A12, A151, ANALMETR:62;
A154: not d2 in A

proof

assume d2 in A ; :: thesis: contradiction
then d19,d29 // d19,d39 by A103, A104, A105, AFF_1:39, AFF_1:41;
then LIN d19,d29,d39 by AFF_1:def 1;
hence contradiction by A91, ANALMETR:40; :: thesis: verum

end;

LIN o9,a39,d49 by A83, ANALMETR:40;
then o9,a39 // o9,d49 by AFF_1:def 1;
then o9,d29 // o9,d49 by A7, A12, A152, DIRAF:40;
then LIN o9,d29,d49 by AFF_1:def 1;
then LIN d29,o9,d49 by AFF_1:6;
then d29,o9 // d29,d49 by AFF_1:def 1;
then o9,d29 // d29,d49 by AFF_1:4;
then o,d2 // d2,d4 by ANALMETR:36;
then A155: d1,d3 _|_ d2,d4 by A87, A153, ANALMETR:62;
K9 = Line (d29,d49) by A100, A134, A135, A136, AFF_1:24;
then K = Line (d2,d4) by ANALMETR:41;
then A156: A _|_ K by A155, A100, A107, A108, ANALMETR:45;
reconsider d19 = d1, d29 = d2, d39 = d3, d49 = d4, b39 = b3, a19 = a1, b19 = b1, a29 = a2 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
LIN d19,d39,b39 by A140, ANALMETR:40;
then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A157: A9 is being_line and
A158: d19 in A9 and
A159: d39 in A9 and
A160: b39 in A9 by AFF_1:21;
A161: d19 <> d39

proof

assume d19 = d39 ; :: thesis: contradiction
then LIN d19,d29,d39 by AFF_1:7;
hence contradiction by A91, ANALMETR:40; :: thesis: verum

end;

reconsider A = A9 as Subset of X ;
LIN d19,d39,b19 by A140, ANALMETR:40;
then A162: b1 in A by A157, A158, A159, A161, AFF_1:25;
A163: not d2 in A

proof

assume d2 in A ; :: thesis: contradiction
then d19,d29 // d19,d39 by A157, A158, A159, AFF_1:39, AFF_1:41;
then d1,d2 // d1,d3 by ANALMETR:36;
hence contradiction by A91, ANALMETR:def 10; :: thesis: verum

end;

A164: d1 <> d4

proof

LIN o9,a39,d49 by A83, ANALMETR:40;
then A165: LIN o9,d49,a39 by AFF_1:6;
LIN o9,d49,o9 by AFF_1:7;
then A166: o9,d49 // o9,a39 by A165, AFF_1:10;
A167: LIN o9,b39,o9 by AFF_1:7;
LIN o9,b29,b39 by A35, ANALMETR:40;
then A168: LIN o9,b39,b29 by AFF_1:6;
LIN o9,b39,d19 by A31, ANALMETR:40;
then LIN o9,d19,b29 by A17, A167, A168, AFF_1:8;
then A169: o9,d19 // o9,b29 by AFF_1:def 1;
assume d1 = d4 ; :: thesis: contradiction
then o9,a39 // o9,b29 by A114, A169, A166, DIRAF:40;
then LIN o9,a39,b29 by AFF_1:def 1;
then LIN a39,b29,o9 by AFF_1:6;
then a39,b29 // a39,o9 by AFF_1:def 1;
then A170: a39,o9 // a39,b29 by AFF_1:4;
LIN o9,a39,a19 by A45, ANALMETR:40;
then LIN a39,o9,a19 by AFF_1:6;
then a39,o9 // a39,a19 by AFF_1:def 1;
then a39,b29 // a39,a19 by A7, A12, A170, DIRAF:40;
then LIN a39,b29,a19 by AFF_1:def 1;
then LIN a39,a19,b29 by AFF_1:6;
hence contradiction by A46, ANALMETR:40; :: thesis: verum

end;

A171: not d4 in A

proof

assume d4 in A ; :: thesis: contradiction
then d19,d49 // d19,d39 by A157, A158, A159, AFF_1:39, AFF_1:41;
then d1,d4 // d1,d3 by ANALMETR:36;
hence contradiction by A117, ANALMETR:def 10; :: thesis: verum

end;

LIN d29,d49,a19 by A140, ANALMETR:40;
then consider K9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A172: K9 is being_line and
A173: d29 in K9 and
A174: d49 in K9 and
A175: a19 in K9 by AFF_1:21;
reconsider K = K9 as Subset of X ;
LIN d29,d49,a29 by A140, ANALMETR:40;
then A176: a2 in K by A100, A172, A173, A174, AFF_1:25;
K9 = Line (d29,d49) by A100, A172, A173, A174, AFF_1:24;
then A177: K = Line (d2,d4) by ANALMETR:41;
A9 = Line (d19,d39) by A157, A158, A159, A161, AFF_1:24;
then A = Line (d1,d3) by ANALMETR:41;
then A _|_ K by A155, A100, A161, A177, ANALMETR:45;
then A178: d1,d4 _|_ b3,a2 by A1, A68, A86, A55, A158, A159, A160, A173, A174, A175, A163, A171, A162, A176;
d1,d2 _|_ a1,b3 by A27, A28, A53, ANALMETR:62;
then d1,d4 _|_ a1,b2 by A2, A131, A81, A104, A105, A106, A135, A136, A137, A154, A130, A156, A110, A138;
then ( a1,b2 // b3,a2 or d1 = d4 ) by A178, ANALMETR:63;
then a19,b29 // b39,a29 by A164, ANALMETR:36;
then a19,b29 // a29,b39 by AFF_1:4;
hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum

end;

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

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

o9,b29 // o9,b39 by A7, A9, A10, A20, AFF_1:39, AFF_1:41;
then A180: LIN o9,b29,b39 by AFF_1:def 1;
assume A181: a1 = a2 ; :: thesis: a1,b2 // a2,b3
a1 <> b1

proof

o9,a19 // o9,a39 by A3, A4, A6, A21, AFF_1:39, AFF_1:41;
then A182: LIN o9,a19,a39 by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A7, A8, A12, A14, A20, A182, AFF_1:25; :: thesis: verum

end;

then a3,b2 // a3,b3 by A18, A19, A181, ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29 = b39 by A3, A6, A7, A11, A12, A21, A180, AFF_1:14, AFF_1:25;
then a19,b29 // a29,b39 by A181, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum

end;

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

A184: not LIN o9,a39,b19

proof

assume LIN o9,a39,b19 ; :: thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; :: thesis: verum

end;

o9,b19 // o9,b39 by A7, A8, A10, A20, AFF_1:39, AFF_1:41;
then A185: LIN o9,b19,b39 by AFF_1:def 1;
assume A186: a1 = a3 ; :: thesis: a1,b2 // a2,b3
then a3,b1 // a3,b3 by A19, ANALMETR:59;
then a39,b19 // a39,b39 by ANALMETR:36;
hence a1,b2 // a2,b3 by A18, A186, A184, A185, AFF_1:14; :: thesis: verum

end;

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

A188: not LIN o9,a39,b19

proof

assume LIN o9,a39,b19 ; :: thesis: contradiction
then LIN o9,b19,a39 by AFF_1:6;
hence contradiction by A7, A8, A12, A16, A20, AFF_1:25; :: thesis: verum

end;

o9,b19 // o9,b29 by A7, A8, A9, A20, AFF_1:39, AFF_1:41;
then A189: LIN o9,b19,b29 by AFF_1:def 1;
assume A190: a2 = a3 ; :: thesis: a1,b2 // a2,b3
then a3,b1 // a3,b2 by A18, ANALMETR:59;
then a39,b19 // a39,b29 by ANALMETR:36;
then a2,b3 // a1,b2 by A19, A190, A188, A189, AFF_1:14;
hence a1,b2 // a2,b3 by ANALMETR:59; :: thesis: verum

end;

assume ( a1 = a2 or a2 = a3 or a1 = a3 ) ; :: thesis: a1,b2 // a2,b3
hence a1,b2 // a2,b3 by A179, A187, A183; :: thesis: verum

end;

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