let X be OrtAfPl; :: thesis: ( X is satisfying_OPAP & X is satisfying_DES implies X is satisfying_PAP )
assume that
A1: X is satisfying_OPAP and
A2: X is satisfying_DES ; :: thesis: X is satisfying_PAP
let o be Element of X; :: according to CONMETR:def 2 :: thesis: for a1, a2, a3, b1, b2, b3 being Element of X
for M, N being Subset of X st M is being_line & N is being_line & 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 & 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 M is being_line & N is being_line & 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 & 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: ( M is being_line & N is being_line & 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 & 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: M is being_line and
A4: N is being_line and
A5: o in M and
A6: a1 in M and
A7: a2 in M and
A8: a3 in M and
A9: o in N and
A10: b1 in N and
A11: b2 in N and
A12: b3 in N and
A13: not b2 in M and
A14: not a3 in N and
A15: o <> a1 and
A16: o <> a2 and
o <> a3 and
A17: o <> b1 and
o <> b2 and
A18: o <> b3 and
A19: a3,b2 // a2,b1 and
A20: 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 #) ;
A21: M9 is being_line by A3, ANALMETR:43;
A22: N9 is being_line by A4, ANALMETR:43;

now :: thesis: ( not M _|_ N implies a1,b2 // a2,b3 )

assume A23: not M _|_ N ; :: thesis: a1,b2 // a2,b3

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

assume that
A25: a1 <> a2 and
A26: a2 <> a3 and
A27: a1 <> a3 ; :: thesis: a1,b2 // a2,b3
A28: ( b1 <> b2 & b2 <> b3 & b1 <> b3 )

proof

A29: now :: thesis: not b1 = b3

A30: not LIN o9,b19,a19

proof

o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A31: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,b19,a19 ; :: thesis: contradiction
then a19 in N9 by A9, A10, A17, A22, AFF_1:25;
hence contradiction by A9, A14, A15, A22, A31, AFF_1:25; :: thesis: verum

end;

assume b1 = b3 ; :: thesis: contradiction
then b1,a1 // b1,a3 by A20, ANALMETR:59;
then A32: b19,a19 // b19,a39 by ANALMETR:36;
o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a39 by AFF_1:def 1;
hence contradiction by A27, A30, A32, AFF_1:14; :: thesis: verum

end;

A33: now :: thesis: not b2 = b3

A34: not LIN o9,b19,a19

proof

o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A35: LIN o9,a19,a39 by AFF_1:def 1;
assume LIN o9,b19,a19 ; :: thesis: contradiction
then a19 in N9 by A9, A10, A17, A22, AFF_1:25;
hence contradiction by A9, A14, A15, A22, A35, AFF_1:25; :: thesis: verum

end;

assume b2 = b3 ; :: thesis: contradiction
then a1,b1 // a2,b1 by A8, A13, A19, A20, ANALMETR:60;
then b1,a1 // b1,a2 by ANALMETR:59;
then A36: b19,a19 // b19,a29 by ANALMETR:36;
o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a29 by AFF_1:def 1;
hence contradiction by A25, A34, A36, AFF_1:14; :: thesis: verum

end;

A37: now :: thesis: not b1 = b2

A38: not LIN o9,b29,a29

proof

assume LIN o9,b29,a29 ; :: thesis: contradiction
then LIN o9,a29,b29 by AFF_1:6;
hence contradiction by A5, A7, A13, A16, A21, AFF_1:25; :: thesis: verum

end;

assume b1 = b2 ; :: thesis: contradiction
then b2,a2 // b2,a3 by A19, ANALMETR:59;
then A39: b29,a29 // b29,a39 by ANALMETR:36;
o9,a29 // o9,a39 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a29,a39 by AFF_1:def 1;
hence contradiction by A26, A38, A39, AFF_1:14; :: thesis: verum

end;

assume ( b1 = b2 or b2 = b3 or b1 = b3 ) ; :: thesis: contradiction
hence contradiction by A37, A33, A29; :: thesis: verum

end;

A40: now :: thesis: ( not a3,b3 _|_ o,b2 implies a1,b2 // a2,b3 )

A41: not LIN b3,b1,a3

proof

assume LIN b3,b1,a3 ; :: thesis: contradiction
then LIN b39,b19,a39 by ANALMETR:40;
hence contradiction by A10, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b39 by AFF_1:def 1;
then A42: LIN o,b2,b3 by ANALMETR:40;
A43: not LIN b2,b1,a3

proof

assume LIN b2,b1,a3 ; :: thesis: contradiction
then LIN b29,b19,a39 by ANALMETR:40;
hence contradiction by A10, A11, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

o9,a39 // o9,a19 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a19 by AFF_1:def 1;
then A44: LIN o,a3,a1 by ANALMETR:40;
consider x being Element of X such that
A45: o,b2 _|_ o,x and
A46: o <> x by ANALMETR:39;
A47: o,x _|_ N by A4, A5, A9, A11, A13, A45, ANALMETR:55;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A48: a39,b39 // b29,e19 and
A49: b29 <> e19 by DIRAF:40;
reconsider x9 = x as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
LIN o9,x9,x9 by AFF_1:7;
then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A50: A9 is being_line and
A51: o9 in A9 and
A52: x9 in A9 and
x9 in A9 by AFF_1:21;
reconsider A = A9 as Subset of X ;
A53: for e1 being Element of X st e1 in A holds
LIN o,x,e1

proof

let e1 be Element of X; :: thesis: ( e1 in A implies LIN o,x,e1 )
assume A54: e1 in A ; :: thesis: LIN o,x,e1
reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
o9,x9 // o9,e19 by A50, A51, A52, A54, AFF_1:39, AFF_1:41;
then LIN o9,x9,e19 by AFF_1:def 1;
hence LIN o,x,e1 by ANALMETR:40; :: thesis: verum

end;

for e1 being Element of X st LIN o,x,e1 holds
e1 in A

proof

let e1 be Element of X; :: thesis: ( LIN o,x,e1 implies e1 in A )
assume A55: LIN o,x,e1 ; :: thesis: e1 in A
reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
LIN o9,x9,e19 by A55, ANALMETR:40;
hence e1 in A by A46, A50, A51, A52, AFF_1:25; :: thesis: verum

end;

then A = Line (o,x) by A53, ANALMETR:def 11;
then A56: A _|_ N by A46, A47, ANALMETR:def 14;
A57: not b2 in A

proof

A58: o9,b29 // o9,b29 by AFF_1:2;
assume b2 in A ; :: thesis: contradiction
then A9 // N9 by A5, A9, A11, A13, A22, A50, A51, A58, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A56, ANALMETR:52; :: thesis: verum

end;

assume A59: not a3,b3 _|_ o,b2 ; :: thesis: a1,b2 // a2,b3
not b29,e19 // A9

proof

assume A60: b29,e19 // A9 ; :: thesis: contradiction
consider d19, d29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A61: d19 <> d29 and
A62: A9 = Line (d19,d29) by A50, AFF_1:def 3;
A63: d29 in A9 by A62, AFF_1:15;
reconsider d1 = d19, d2 = d29 as Element of X ;
d19,d29 // d19,d29 by AFF_1:2;
then d19,d29 // A9 by A61, A62, AFF_1:def 4;
then b29,e19 // d19,d29 by A50, A60, AFF_1:31;
then a39,b39 // d19,d29 by A48, A49, AFF_1:5;
then A64: a3,b3 // d1,d2 by ANALMETR:36;
d19 in A9 by A62, AFF_1:15;
then d1,d2 _|_ o,b2 by A9, A11, A56, A63, ANALMETR:56;
hence contradiction by A59, A61, A64, ANALMETR:62; :: thesis: verum

end;

then consider c39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A65: c39 in A9 and
A66: LIN b29,e19,c39 by A50, AFF_1:59;
b29,e19 // b29,c39 by A66, AFF_1:def 1;
then A67: a39,b39 // b29,c39 by A48, A49, AFF_1:5;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A68: c39,a39 // a19,e19 and
A69: a19 <> e19 by DIRAF:40;
not a19,e19 // A9

proof

A70: c39 <> o9

proof

assume c39 = o9 ; :: thesis: contradiction
then A71: a3,b3 // b2,o by A67, ANALMETR:36;
b29,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then b2,o // b2,b3 by ANALMETR:36;
then a3,b3 // b2,b3 by A5, A13, A71, ANALMETR:60;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

assume A72: a19,e19 // A9 ; :: thesis: contradiction
A73: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A50, A51, A65, AFF_1:40, AFF_1:41;
then a19,e19 // o9,c39 by A50, A72, AFF_1:31;
then c39,a39 // o9,c39 by A68, A69, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A50, A51, A65, A70, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A73, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

then consider c19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A74: c19 in A9 and
A75: LIN a19,e19,c19 by A50, AFF_1:59;
reconsider c1 = c19 as Element of X ;
reconsider c3 = c39 as Element of X ;
a19,e19 // a19,c19 by A75, AFF_1:def 1;
then A76: c39,a39 // a19,c19 by A68, A69, AFF_1:5;
then A77: c3,a3 // a1,c1 by ANALMETR:36;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A78: c39,a39 // a29,e19 and
A79: a29 <> e19 by DIRAF:40;
not a29,e19 // A9

proof

A80: c39 <> o9

proof

assume c39 = o9 ; :: thesis: contradiction
then A81: a3,b3 // b2,o by A67, ANALMETR:36;
b29,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then b2,o // b2,b3 by ANALMETR:36;
then a3,b3 // b2,b3 by A5, A13, A81, ANALMETR:60;
then b3,b2 // b3,a3 by ANALMETR:59;
then LIN b3,b2,a3 by ANALMETR:def 10;
then LIN b39,b29,a39 by ANALMETR:40;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

assume A82: a29,e19 // A9 ; :: thesis: contradiction
A83: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A50, A51, A65, AFF_1:40, AFF_1:41;
then a29,e19 // o9,c39 by A50, A82, AFF_1:31;
then c39,a39 // o9,c39 by A78, A79, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A50, A51, A65, A80, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A83, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

then consider c29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A84: c29 in A9 and
A85: LIN a29,e19,c29 by A50, AFF_1:59;
reconsider c2 = c29 as Element of X ;
a29,e19 // a29,c29 by A85, AFF_1:def 1;
then A86: c39,a39 // a29,c29 by A78, A79, AFF_1:5;
then A87: c3,a3 // a2,c2 by ANALMETR:36;
A88: ( o <> c3 & o <> c2 & o <> c1 )

proof

A89: now :: thesis: not o = c3

assume A90: o = c3 ; :: thesis: contradiction
b29,o9 // b39,b29 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then a39,b39 // b39,b29 by A5, A13, A67, A90, AFF_1:5;
then b39,b29 // b39,a39 by AFF_1:4;
then LIN b39,b29,a39 by AFF_1:def 1;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

A91: now :: thesis: ( not o = c2 & not o = c1 )

a19,o9 // a19,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A92: a1,o // a1,a3 by ANALMETR:36;
assume ( o = c2 or o = c1 ) ; :: thesis: contradiction
then A93: ( c3,a3 // a1,o or c3,a3 // a2,o ) by A76, A86, ANALMETR:36;
a29,o9 // a19,a39 by A5, A6, A7, A8, A21, AFF_1:39, AFF_1:41;
then a2,o // a1,a3 by ANALMETR:36;
then c3,a3 // a1,a3 by A15, A16, A93, A92, ANALMETR:60;
then a3,a1 // a3,c3 by ANALMETR:59;
then LIN a3,a1,c3 by ANALMETR:def 10;
then LIN a39,a19,c39 by ANALMETR:40;
then A94: c39 in M9 by A6, A8, A21, A27, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A65, A89, A94, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

assume ( o = c3 or o = c2 or o = c1 ) ; :: thesis: contradiction
hence contradiction by A89, A91; :: thesis: verum

end;

A95: not c3 in N

proof

A96: o9,c39 // o9,c39 by AFF_1:2;
assume c3 in N ; :: thesis: contradiction
then A9 // N9 by A9, A22, A50, A51, A65, A88, A96, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A56, ANALMETR:52; :: thesis: verum

end;

A97: not LIN a3,a2,c3

proof

assume LIN a3,a2,c3 ; :: thesis: contradiction
then LIN a39,a29,c39 by ANALMETR:40;
then A98: c39 in M9 by A7, A8, A21, A26, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A65, A88, A98, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

A99: not LIN a3,a1,c3

proof

assume LIN a3,a1,c3 ; :: thesis: contradiction
then LIN a39,a19,c39 by ANALMETR:40;
then A100: c39 in M9 by A6, A8, A21, A27, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A65, A88, A100, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

A101: not LIN a1,a2,c1

proof

assume LIN a1,a2,c1 ; :: thesis: contradiction
then LIN a19,a29,c19 by ANALMETR:40;
then A102: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then M9 // A9 by A5, A21, A50, A51, A74, A88, A102, AFF_1:38;
then M // A by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a29 by AFF_1:def 1;
then A103: LIN o,a1,a2 by ANALMETR:40;
o9,b29 // o9,b19 by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b19 by AFF_1:def 1;
then A104: LIN o,b2,b1 by ANALMETR:40;
o9,c19 // o9,c29 by A50, A51, A74, A84, AFF_1:39, AFF_1:41;
then LIN o9,c19,c29 by AFF_1:def 1;
then A105: LIN o,c1,c2 by ANALMETR:40;
o9,c39 // o9,c29 by A50, A51, A65, A84, AFF_1:39, AFF_1:41;
then LIN o9,c39,c29 by AFF_1:def 1;
then A106: LIN o,c3,c2 by ANALMETR:40;
o9,c39 // o9,c19 by A50, A51, A65, A74, AFF_1:39, AFF_1:41;
then LIN o9,c39,c19 by AFF_1:def 1;
then A107: LIN o,c3,c1 by ANALMETR:40;
c3 <> a3

proof

A108: o9,a39 // o9,a39 by AFF_1:2;
assume c3 = a3 ; :: thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A65, A108, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

then a1,c1 // a2,c2 by A77, A87, ANALMETR:60;
then A109: c1,a1 // c2,a2 by ANALMETR:59;
A110: not LIN c1,c2,b2

proof

A111: c19 <> c29

proof

A112: c3 <> a3

proof

A113: o9,c39 // o9,c39 by AFF_1:2;
assume c3 = a3 ; :: thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A50, A51, A65, A113, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

assume c19 = c29 ; :: thesis: contradiction
then a1,c1 // a2,c1 by A77, A87, A112, ANALMETR:60;
then c1,a2 // c1,a1 by ANALMETR:59;
then LIN c1,a2,a1 by ANALMETR:def 10;
then LIN c19,a29,a19 by ANALMETR:40;
then LIN a19,a29,c19 by AFF_1:6;
then A114: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5, A21, A50, A51, A74, A88, A114, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A56, ANALMETR:52; :: thesis: verum

end;

assume LIN c1,c2,b2 ; :: thesis: contradiction
then LIN c19,c29,b29 by ANALMETR:40;
then b29 in A9 by A50, A74, A84, A111, AFF_1:25;
then A9 = N9 by A5, A9, A11, A13, A22, A50, A51, AFF_1:18;
then A9 // N9 by A22, AFF_1:41;
then A // N by ANALMETR:46;
hence contradiction by A56, ANALMETR:52; :: thesis: verum

end;

o9,a39 // o9,a29 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a29 by AFF_1:def 1;
then A115: LIN o,a3,a2 by ANALMETR:40;
o9,b39 // o9,b19 by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b39,b19 by AFF_1:def 1;
then A116: LIN o,b3,b1 by ANALMETR:40;
a3,c3 // a1,c1 by A77, ANALMETR:59;
then b3,c3 // b1,c1 by A2, A9, A14, A15, A17, A18, A20, A88, A99, A41, A44, A116, A107, CONAFFM:def 1;
then A117: c3,b3 // c1,b1 by ANALMETR:59;
a3,c3 // a2,c2 by A87, ANALMETR:59;
then b2,c3 // b1,c2 by A2, A5, A9, A13, A14, A16, A17, A19, A88, A115, A104, A106, A43, A97, CONAFFM:def 1;
then c3,b2 // c2,b1 by ANALMETR:59;
then c1,b2 // c2,b3 by A1, A9, A10, A11, A12, A17, A18, A51, A56, A65, A74, A84, A88, A117, A57, A95;
hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A88, A103, A42, A105, A101, A110, A109, CONAFFM:def 1; :: thesis: verum

end;

now :: thesis: ( a3,b3 _|_ o,b2 implies a1,b2 // a2,b3 )

o9,a19 // o9,a29 by A5, A6, A7, A21, AFF_1:39, AFF_1:41;
then LIN o9,a19,a29 by AFF_1:def 1;
then A118: LIN o,a1,a2 by ANALMETR:40;
o9,b29 // o9,b19 by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b19 by AFF_1:def 1;
then A119: LIN o,b2,b1 by ANALMETR:40;
o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b29,b39 by AFF_1:def 1;
then A120: LIN o,b2,b3 by ANALMETR:40;
A121: ( not LIN b3,b1,a3 & not LIN b2,b1,a3 )

proof

assume ( LIN b3,b1,a3 or LIN b2,b1,a3 ) ; :: thesis: contradiction
then ( LIN b39,b19,a39 or LIN b29,b19,a39 ) by ANALMETR:40;
hence contradiction by A10, A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

o9,a39 // o9,a29 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a29 by AFF_1:def 1;
then A122: LIN o,a3,a2 by ANALMETR:40;
o9,b39 // o9,b19 by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then LIN o9,b39,b19 by AFF_1:def 1;
then A123: LIN o,b3,b1 by ANALMETR:40;
o9,a39 // o9,a19 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then LIN o9,a39,a19 by AFF_1:def 1;
then A124: LIN o,a3,a1 by ANALMETR:40;
consider x being Element of X such that
A125: o,b2 _|_ o,x and
A126: o <> x by ANALMETR:39;
A127: o,x _|_ N by A4, A5, A9, A11, A13, A125, ANALMETR:55;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A128: a39,b29 // b39,e19 and
A129: b39 <> e19 by DIRAF:40;
reconsider x9 = x as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
LIN o9,x9,x9 by AFF_1:7;
then consider A9 being Subset of AffinStruct(# the carrier of X, the CONGR of X #) such that
A130: A9 is being_line and
A131: o9 in A9 and
A132: x9 in A9 and
x9 in A9 by AFF_1:21;
reconsider A = A9 as Subset of X ;
A133: for e1 being Element of X st e1 in A holds
LIN o,x,e1

proof

let e1 be Element of X; :: thesis: ( e1 in A implies LIN o,x,e1 )
assume A134: e1 in A ; :: thesis: LIN o,x,e1
reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
o9,x9 // o9,e19 by A130, A131, A132, A134, AFF_1:39, AFF_1:41;
then LIN o9,x9,e19 by AFF_1:def 1;
hence LIN o,x,e1 by ANALMETR:40; :: thesis: verum

end;

for e1 being Element of X st LIN o,x,e1 holds
e1 in A

proof

let e1 be Element of X; :: thesis: ( LIN o,x,e1 implies e1 in A )
assume A135: LIN o,x,e1 ; :: thesis: e1 in A
reconsider e19 = e1 as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
LIN o9,x9,e19 by A135, ANALMETR:40;
hence e1 in A by A126, A130, A131, A132, AFF_1:25; :: thesis: verum

end;

then A = Line (o,x) by A133, ANALMETR:def 11;
then A136: A _|_ N by A126, A127, ANALMETR:def 14;
assume A137: a3,b3 _|_ o,b2 ; :: thesis: a1,b2 // a2,b3
not b39,e19 // A9

proof

assume A138: b39,e19 // A9 ; :: thesis: contradiction
consider d19, d29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A139: d19 <> d29 and
A140: A9 = Line (d19,d29) by A130, AFF_1:def 3;
A141: d29 in A9 by A140, AFF_1:15;
reconsider d1 = d19, d2 = d29 as Element of X ;
d19,d29 // d19,d29 by AFF_1:2;
then d19,d29 // A9 by A139, A140, AFF_1:def 4;
then b39,e19 // d19,d29 by A130, A138, AFF_1:31;
then a39,b29 // d19,d29 by A128, A129, AFF_1:5;
then A142: a3,b2 // d1,d2 by ANALMETR:36;
d19 in A9 by A140, AFF_1:15;
then d1,d2 _|_ o,b2 by A9, A11, A136, A141, ANALMETR:56;
then a3,b2 _|_ o,b2 by A139, A142, ANALMETR:62;
then a3,b2 // a3,b3 by A5, A13, A137, ANALMETR:63;
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 A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

then consider c39 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A143: c39 in A9 and
A144: LIN b39,e19,c39 by A130, AFF_1:59;
A145: b39,e19 // b39,c39 by A144, AFF_1:def 1;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A146: c39,a39 // a29,e19 and
A147: a29 <> e19 by DIRAF:40;
not a29,e19 // A9

proof

A148: c39 <> o9

proof

assume c39 = o9 ; :: thesis: contradiction
then A149: a39,b29 // b39,o9 by A128, A129, A145, AFF_1:5;
b39,o9 // b39,b29 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then a39,b29 // b39,b29 by A18, A149, AFF_1:5;
then b29,b39 // b29,a39 by AFF_1:4;
then LIN b29,b39,a39 by AFF_1:def 1;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

assume A150: a29,e19 // A9 ; :: thesis: contradiction
A151: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A130, A131, A143, AFF_1:40, AFF_1:41;
then a29,e19 // o9,c39 by A130, A150, AFF_1:31;
then c39,a39 // o9,c39 by A146, A147, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A130, A131, A143, A148, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A151, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

then consider c29 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A152: c29 in A9 and
A153: LIN a29,e19,c29 by A130, AFF_1:59;
reconsider c3 = c39 as Element of X ;
reconsider c2 = c29 as Element of X ;
a29,e19 // a29,c29 by A153, AFF_1:def 1;
then c39,a39 // a29,c29 by A146, A147, AFF_1:5;
then A154: c3,a3 // a2,c2 by ANALMETR:36;
then A155: a3,c3 // a2,c2 by ANALMETR:59;
consider e19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A156: c39,a39 // a19,e19 and
A157: a19 <> e19 by DIRAF:40;
not a19,e19 // A9

proof

A158: c39 <> o9

proof

assume c39 = o9 ; :: thesis: contradiction
then A159: a39,b29 // b39,o9 by A128, A129, A145, AFF_1:5;
b39,o9 // b39,b29 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then a39,b29 // b39,b29 by A18, A159, AFF_1:5;
then b29,b39 // b29,a39 by AFF_1:4;
then LIN b29,b39,a39 by AFF_1:def 1;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

assume A160: a19,e19 // A9 ; :: thesis: contradiction
A161: o9,a39 // o9,a39 by AFF_1:2;
o9,c39 // A9 by A130, A131, A143, AFF_1:40, AFF_1:41;
then a19,e19 // o9,c39 by A130, A160, AFF_1:31;
then c39,a39 // o9,c39 by A156, A157, AFF_1:5;
then c39,o9 // c39,a39 by AFF_1:4;
then LIN c39,o9,a39 by AFF_1:def 1;
then a39 in A9 by A130, A131, A143, A158, AFF_1:25;
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A161, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

then consider c19 being Element of AffinStruct(# the carrier of X, the CONGR of X #) such that
A162: c19 in A9 and
A163: LIN a19,e19,c19 by A130, AFF_1:59;
reconsider c1 = c19 as Element of X ;
a19,e19 // a19,c19 by A163, AFF_1:def 1;
then c39,a39 // a19,c19 by A156, A157, AFF_1:5;
then A164: c3,a3 // a1,c1 by ANALMETR:36;
then A165: a3,c3 // a1,c1 by ANALMETR:59;
A166: a39,b29 // b39,c39 by A128, A129, A145, AFF_1:5;
A167: ( o <> c3 & o <> c2 & o <> c1 )

proof

A168: now :: thesis: not o = c3

assume o = c3 ; :: thesis: contradiction
then A169: a3,b2 // b3,o by A166, ANALMETR:36;
b39,o9 // b29,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then b3,o // b2,b3 by ANALMETR:36;
then a3,b2 // b2,b3 by A18, A169, ANALMETR:60;
then b2,b3 // b2,a3 by ANALMETR:59;
then LIN b2,b3,a3 by ANALMETR:def 10;
then LIN b29,b39,a39 by ANALMETR:40;
hence contradiction by A11, A12, A14, A22, A28, AFF_1:25; :: thesis: verum

end;

A170: now :: thesis: ( not o = c2 & not o = c1 )

a29,o9 // a29,a39 by A5, A7, A8, A21, AFF_1:39, AFF_1:41;
then A171: a2,o // a2,a3 by ANALMETR:36;
assume ( o = c2 or o = c1 ) ; :: thesis: contradiction
then A172: ( a3,c3 // a2,o or a3,c3 // a1,o ) by A154, A164, ANALMETR:59;
a19,o9 // a29,a39 by A5, A6, A7, A8, A21, AFF_1:39, AFF_1:41;
then a1,o // a2,a3 by ANALMETR:36;
then a3,c3 // a2,a3 by A15, A16, A172, A171, ANALMETR:60;
then a3,a2 // a3,c3 by ANALMETR:59;
then LIN a3,a2,c3 by ANALMETR:def 10;
then LIN a39,a29,c39 by ANALMETR:40;
then A173: c39 in M9 by A7, A8, A21, A26, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A143, A168, A173, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

assume ( o = c3 or o = c2 or o = c1 ) ; :: thesis: contradiction
hence contradiction by A168, A170; :: thesis: verum

end;

A174: not c3 in N

proof

A175: o9,c39 // o9,c39 by AFF_1:2;
assume c3 in N ; :: thesis: contradiction
then A9 // N9 by A9, A22, A130, A131, A143, A167, A175, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A136, ANALMETR:52; :: thesis: verum

end;

A176: not LIN a1,a2,c1

proof

assume LIN a1,a2,c1 ; :: thesis: contradiction
then LIN a19,a29,c19 by ANALMETR:40;
then A177: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A162, A167, A177, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

A178: ( not LIN a3,a1,c3 & not LIN a3,a2,c3 )

proof

assume ( LIN a3,a1,c3 or LIN a3,a2,c3 ) ; :: thesis: contradiction
then ( LIN a39,a19,c39 or LIN a39,a29,c39 ) by ANALMETR:40;
then A179: ( c39 in M9 or c39 in M9 ) by A6, A7, A8, A21, A26, A27, AFF_1:25;
o9,c39 // o9,c39 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A143, A167, A179, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

A180: not b2 in A

proof

A181: o9,b29 // o9,b29 by AFF_1:2;
assume b2 in A ; :: thesis: contradiction
then A9 // N9 by A5, A9, A11, A13, A22, A130, A131, A181, AFF_1:38;
then A // N by ANALMETR:46;
hence contradiction by A136, ANALMETR:52; :: thesis: verum

end;

A182: not LIN c1,c2,b2

proof

A183: c19 <> c29

proof

A184: a3 <> c3

proof

A185: o9,c39 // o9,c39 by AFF_1:2;
assume a3 = c3 ; :: thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A143, A185, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

assume c19 = c29 ; :: thesis: contradiction
then a2,c1 // a1,c1 by A155, A165, A184, ANALMETR:60;
then c1,a1 // c1,a2 by ANALMETR:59;
then LIN c1,a1,a2 by ANALMETR:def 10;
then LIN c19,a19,a29 by ANALMETR:40;
then LIN a19,a29,c19 by AFF_1:6;
then A186: c19 in M9 by A6, A7, A21, A25, AFF_1:25;
o9,c19 // o9,c19 by AFF_1:2;
then A9 // M9 by A5, A21, A130, A131, A162, A167, A186, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

assume LIN c1,c2,b2 ; :: thesis: contradiction
then LIN c19,c29,b29 by ANALMETR:40;
hence contradiction by A130, A152, A162, A180, A183, AFF_1:25; :: thesis: verum

end;

o9,c19 // o9,c29 by A130, A131, A152, A162, AFF_1:39, AFF_1:41;
then LIN o9,c19,c29 by AFF_1:def 1;
then A187: LIN o,c1,c2 by ANALMETR:40;
a3 <> c3

proof

A188: o9,a39 // o9,a39 by AFF_1:2;
assume a3 = c3 ; :: thesis: contradiction
then A9 // M9 by A5, A8, A9, A14, A21, A130, A131, A143, A188, AFF_1:38;
then A // M by ANALMETR:46;
hence contradiction by A23, A136, ANALMETR:52; :: thesis: verum

end;

then a2,c2 // a1,c1 by A155, A165, ANALMETR:60;
then A189: c1,a1 // c2,a2 by ANALMETR:59;
o9,c39 // o9,c19 by A130, A131, A143, A162, AFF_1:39, AFF_1:41;
then LIN o9,c39,c19 by AFF_1:def 1;
then LIN o,c3,c1 by ANALMETR:40;
then b3,c3 // b1,c1 by A2, A9, A14, A15, A17, A18, A20, A165, A167, A121, A178, A124, A123, CONAFFM:def 1;
then A190: c3,b3 // c1,b1 by ANALMETR:59;
o9,c39 // o9,c29 by A130, A131, A143, A152, AFF_1:39, AFF_1:41;
then LIN o9,c39,c29 by AFF_1:def 1;
then LIN o,c3,c2 by ANALMETR:40;
then b2,c3 // b1,c2 by A2, A5, A9, A13, A14, A16, A17, A19, A155, A167, A121, A178, A122, A119, CONAFFM:def 1;
then c3,b2 // c2,b1 by ANALMETR:59;
then c1,b2 // c2,b3 by A1, A9, A10, A11, A12, A17, A18, A131, A136, A143, A152, A162, A167, A190, A180, A174;
hence a1,b2 // a2,b3 by A2, A5, A13, A15, A16, A18, A167, A118, A120, A187, A176, A182, A189, CONAFFM:def 1; :: thesis: verum

end;

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

end;

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

A192: not LIN o9,a39,b39

proof

assume LIN o9,a39,b39 ; :: thesis: contradiction
then LIN o9,b39,a39 by AFF_1:6;
hence contradiction by A9, A12, A14, A18, A22, AFF_1:25; :: thesis: verum

end;

o9,b39 // o9,b19 by A9, A10, A12, A22, AFF_1:39, AFF_1:41;
then A193: LIN o9,b39,b19 by AFF_1:def 1;
assume A194: a1 = a3 ; :: thesis: a1,b2 // a2,b3
then a39,b39 // a39,b19 by A20, ANALMETR:36;
hence a1,b2 // a2,b3 by A19, A194, A192, A193, AFF_1:14; :: thesis: verum

end;

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

o9,b29 // o9,b39 by A9, A11, A12, A22, AFF_1:39, AFF_1:41;
then A196: LIN o9,b29,b39 by AFF_1:def 1;
assume A197: a1 = a2 ; :: thesis: a1,b2 // a2,b3
a1 <> b1

proof

o9,a19 // o9,a39 by A5, A6, A8, A21, AFF_1:39, AFF_1:41;
then A198: LIN o9,a19,a39 by AFF_1:def 1;
assume a1 = b1 ; :: thesis: contradiction
hence contradiction by A9, A10, A14, A15, A22, A198, AFF_1:25; :: thesis: verum

end;

then a3,b2 // a3,b3 by A19, A20, A197, ANALMETR:60;
then a39,b29 // a39,b39 by ANALMETR:36;
then b29 = b39 by A5, A8, A9, A13, A14, A21, A196, AFF_1:14, AFF_1:25;
then a19,b29 // a29,b39 by A197, AFF_1:2;
hence a1,b2 // a2,b3 by ANALMETR:36; :: thesis: verum

end;

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

o9,b29 // o9,b19 by A9, A10, A11, A22, AFF_1:39, AFF_1:41;
then A199: LIN o9,b29,b19 by AFF_1:def 1;
assume A200: a2 = a3 ; :: thesis: a1,b2 // a2,b3
then a39,b29 // a39,b19 by A19, ANALMETR:36;
then b29 = b19 by A5, A8, A9, A13, A14, A21, A199, AFF_1:14, AFF_1:25;
hence a1,b2 // a2,b3 by A20, A200, ANALMETR:59; :: thesis: verum

end;

hence a1,b2 // a2,b3 by A195, A191, A24; :: thesis: verum

end;

hence a1,b2 // a2,b3 by A1, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20; :: thesis: verum