/
afvect01.miz
655 lines (640 loc) · 30.1 KB
/
afvect01.miz
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
:: One-Dimensional Congruence of Segments, Basic Facts and Midpoint Relation
:: by Barbara Konstanta, Urszula Kowieska, Grzegorz Lewandowski and
:: Krzysztof Pra\.zmowski
::
:: Received October 4, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies AFVECT0, SUBSET_1, XBOOLE_0, RELAT_1, ZFMISC_1, ANALOAF, PARSP_1,
DIRAF, STRUCT_0, AFVECT01;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ANALOAF, DIRAF,
AFVECT0, RELSET_1;
constructors DOMAIN_1, DIRAF, AFVECT0;
registrations XBOOLE_0, STRUCT_0, AFVECT0;
requirements SUBSET, BOOLE;
theorems ZFMISC_1, AFVECT0, STRUCT_0, ANALOAF, DIRAF, XTUPLE_0;
schemes RELSET_1;
begin
registration
let C1 being non empty set;
let C2 being (Relation of [: C1 , C1 :]);
cluster AffinStruct (# C1 , C2 #) -> non empty;
coherence;
end;
L2: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds ((R2 , R4 '||' R4 , R6 & R2 <> R6) implies R2 , R4 // R4 , R6)))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
assume that
L3: R2 , R4 '||' R4 , R6
and
L4: R2 <> R6;
L5: (not R2 , R4 // R6 , R4) by L4 , AFVECT0:4 , AFVECT0:7;
thus L6: thesis by L5 , L3 , DIRAF:def 4;
end;
L7: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (R2 , R4 // R4 , R2 iff (ex R8 being (Element of R1) st (ex R10 being (Element of R1) st (R2 , R4 '||' R8 , R10 & R2 , R8 '||' R8 , R4 & R2 , R10 '||' R10 , R4)))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
L8:
now
given R8 being (Element of R1) , R10 being (Element of R1) such that
L9: R2 , R4 '||' R8 , R10
and
L10: R2 , R8 '||' R8 , R4
and
L11: R2 , R10 '||' R10 , R4;
L12:
now
L13:
now
assume L14: MDist R8 , R10;
L15: (R2 , R4 // R8 , R10 or R2 , R4 // R10 , R8) by L9 , DIRAF:def 4;
L16: MDist R2 , R4 by L15 , L14 , AFVECT0:3 , AFVECT0:15;
thus L17: R2 , R4 // R4 , R2 by L16 , AFVECT0:def 2;
end;
assume L18: R2 <> R4;
L19: R2 , R10 // R10 , R4 by L18 , L11 , L2;
L20: Mid R2 , R10 , R4 by L19 , AFVECT0:def 3;
L21:
now
assume L22: R8 = R10;
L23: R2 , R4 // R8 , R8 by L22 , L9 , DIRAF:def 4;
thus L24: contradiction by L23 , L18 , AFVECT0:def 1;
end;
L25: R2 , R8 // R8 , R4 by L10 , L18 , L2;
L26: Mid R2 , R8 , R4 by L25 , AFVECT0:def 3;
thus L27: R2 , R4 // R4 , R2 by L26 , L20 , L21 , L13 , AFVECT0:20;
end;
thus L28: R2 , R4 // R4 , R2 by L12 , AFVECT0:2;
end;
L29:
now
assume L30: R2 , R4 // R4 , R2;
L31:
now
assume L32: R2 <> R4;
L33: MDist R2 , R4 by L32 , L30 , AFVECT0:def 2;
consider R8 being (Element of R1) such that L34: Mid R2 , R8 , R4 by AFVECT0:19;
L35: R2 , R8 // R8 , R4 by L34 , AFVECT0:def 3;
consider R10 being (Element of R1) such that L36: R2 , R4 // R8 , R10 by AFVECT0:def 1;
take D1 = R8;
take D2 = R10;
L37: Mid R2 , D2 , R4 by L34 , L36 , L33 , AFVECT0:15 , AFVECT0:23;
L38: R2 , D2 // D2 , R4 by L37 , AFVECT0:def 3;
thus L39: (R2 , R4 '||' D1 , D2 & R2 , D1 '||' D1 , R4 & R2 , D2 '||' D2 , R4) by L38 , L36 , L35 , DIRAF:def 4;
end;
L40:
now
assume L41: R2 = R4;
take D3 = R2;
take D4 = R2;
L42: R2 , R4 // D3 , D4 by L41 , AFVECT0:2;
thus L43: (R2 , R4 '||' D3 , D4 & R2 , D3 '||' D3 , R4 & R2 , D4 '||' D4 , R4) by L42 , L41 , DIRAF:def 4;
end;
thus L44: (ex R8 being (Element of R1) st (ex R10 being (Element of R1) st (R2 , R4 '||' R8 , R10 & R2 , R8 '||' R8 , R4 & R2 , R10 '||' R10 , R4))) by L40 , L31;
end;
thus L45: thesis by L29 , L8;
end;
L46: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R7 being (Element of R1) holds (R2 , R4 '||' R6 , R7 implies R4 , R2 '||' R6 , R7))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R7 being (Element of R1);
assume L47: R2 , R4 '||' R6 , R7;
L48: (R2 , R4 // R6 , R7 or R2 , R4 // R7 , R6) by L47 , DIRAF:def 4;
L49: (R4 , R2 // R7 , R6 or R4 , R2 // R6 , R7) by L48 , AFVECT0:7;
thus L50: thesis by L49 , DIRAF:def 4;
end;
L51: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds R2 , R4 '||' R4 , R2)))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
L52: R2 , R4 // R2 , R4 by AFVECT0:1;
thus L53: thesis by L52 , DIRAF:def 4;
end;
L54: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R8 being (Element of R1) holds (R2 , R4 '||' R8 , R8 implies R2 = R4)))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R8 being (Element of R1);
assume L55: R2 , R4 '||' R8 , R8;
L56: R2 , R4 // R8 , R8 by L55 , DIRAF:def 4;
thus L57: thesis by L56 , AFVECT0:def 1;
end;
L58: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R7 being (Element of R1) holds (for R8 being (Element of R1) holds (for R10 being (Element of R1) holds ((R2 , R4 '||' R8 , R10 & R6 , R7 '||' R8 , R10) implies R2 , R4 '||' R6 , R7))))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R7 being (Element of R1);
let R8 being (Element of R1);
let R10 being (Element of R1);
assume L59: (R2 , R4 '||' R8 , R10 & R6 , R7 '||' R8 , R10);
L60: ((R2 , R4 // R8 , R10 & R6 , R7 // R8 , R10) or (R2 , R4 // R8 , R10 & R6 , R7 // R10 , R8) or (R2 , R4 // R10 , R8 & R6 , R7 // R8 , R10) or (R2 , R4 // R10 , R8 & R6 , R7 // R10 , R8)) by L59 , DIRAF:def 4;
L61: (R2 , R4 // R6 , R7 or (R2 , R4 // R8 , R10 & R7 , R6 // R8 , R10) or (R2 , R4 // R10 , R8 & R7 , R6 // R10 , R8)) by L60 , AFVECT0:7 , AFVECT0:def 1;
L62: (R2 , R4 // R6 , R7 or R2 , R4 // R7 , R6) by L61 , AFVECT0:def 1;
thus L63: thesis by L62 , DIRAF:def 4;
end;
L64: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R6 being (Element of R1) holds (ex R4 being (Element of R1) st R2 , R4 '||' R4 , R6))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R6 being (Element of R1);
consider R4 being (Element of R1) such that L65: R2 , R4 // R4 , R6 by AFVECT0:def 1;
take R4;
thus L66: thesis by L65 , DIRAF:def 4;
end;
L67: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R3 being (Element of R1) holds (for R4 being (Element of R1) holds (for R5 being (Element of R1) holds (for R8 being (Element of R1) holds ((R2 <> R3 & R4 <> R5 & R8 , R2 '||' R8 , R3 & R8 , R4 '||' R8 , R5) implies R2 , R4 '||' R3 , R5)))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R3 being (Element of R1);
let R4 being (Element of R1);
let R5 being (Element of R1);
let R8 being (Element of R1);
assume that
L68: R2 <> R3
and
L69: R4 <> R5
and
L70: R8 , R2 '||' R8 , R3
and
L71: R8 , R4 '||' R8 , R5;
L72: R4 , R8 // R8 , R5 by L69 , L71 , L2 , L46;
L73: Mid R4 , R8 , R5 by L72 , AFVECT0:def 3;
L74: R2 , R8 // R8 , R3 by L68 , L70 , L2 , L46;
L75: Mid R2 , R8 , R3 by L74 , AFVECT0:def 3;
L76: R2 , R4 // R5 , R3 by L75 , L73 , AFVECT0:25;
thus L77: thesis by L76 , DIRAF:def 4;
end;
L78: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (R2 = R4 or (ex R6 being (Element of R1) st ((R2 <> R6 & R2 , R4 '||' R4 , R6) or (ex R8 being (Element of R1) st (ex R9 being (Element of R1) st (R8 <> R9 & R2 , R4 '||' R8 , R9 & R2 , R8 '||' R8 , R4 & R2 , R9 '||' R9 , R4)))))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
consider R6 being (Element of R1) such that L79: R2 , R4 // R4 , R6 by AFVECT0:def 1;
L80:
now
assume L81: R2 = R6;
consider R8 being (Element of R1), R9 being (Element of R1) such that L82: R2 , R4 '||' R8 , R9 and L83: (R2 , R8 '||' R8 , R4 & R2 , R9 '||' R9 , R4) by L81 , L79 , L7;
L84: (R8 = R9 implies R2 = R4) by L82 , L54;
thus L85: (R2 = R4 or (ex R8 being (Element of R1) st (ex R9 being (Element of R1) st (R8 <> R9 & R2 , R4 '||' R8 , R9 & R2 , R8 '||' R8 , R4 & R2 , R9 '||' R9 , R4)))) by L84 , L82 , L83;
end;
L86:
now
assume L87: R2 <> R6;
L88: R2 , R4 '||' R4 , R6 by L79 , DIRAF:def 4;
thus L89: (ex R6 being (Element of R1) st (R2 <> R6 & R2 , R4 '||' R4 , R6)) by L88 , L87;
end;
thus L90: thesis by L86 , L80;
end;
L91: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R5 being (Element of R1) holds (for R8 being (Element of R1) holds (for R9 being (Element of R1) holds (for R6 being (Element of R1) holds ((R2 , R4 '||' R4 , R6 & R4 , R5 '||' R8 , R9 & R4 , R8 '||' R8 , R5 & R4 , R9 '||' R9 , R5) implies R2 , R5 '||' R5 , R6))))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R5 being (Element of R1);
let R8 being (Element of R1);
let R9 being (Element of R1);
let R6 being (Element of R1);
assume that
L92: R2 , R4 '||' R4 , R6
and
L93: (R4 , R5 '||' R8 , R9 & R4 , R8 '||' R8 , R5 & R4 , R9 '||' R9 , R5);
L94: R4 , R5 // R5 , R4 by L93 , L7;
L95:
now
assume L96: R2 , R4 // R4 , R6;
L97: Mid R2 , R4 , R6 by L96 , AFVECT0:def 3;
L98:
now
assume L99: MDist R4 , R5;
L100: Mid R2 , R5 , R6 by L99 , L97 , AFVECT0:23;
L101: R2 , R5 // R5 , R6 by L100 , AFVECT0:def 3;
thus L102: thesis by L101 , DIRAF:def 4;
end;
L103: (R4 = R5 implies thesis) by L96 , DIRAF:def 4;
thus L104: thesis by L103 , L94 , L98 , AFVECT0:def 2;
end;
L105:
now
assume L106: R2 , R4 // R6 , R4;
L107: R2 = R6 by L106 , AFVECT0:4 , AFVECT0:7;
L108: R2 , R5 // R6 , R5 by L107 , AFVECT0:1;
thus L109: thesis by L108 , DIRAF:def 4;
end;
thus L110: thesis by L105 , L92 , L95 , DIRAF:def 4;
end;
L111: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R5 being (Element of R1) holds (for R6 being (Element of R1) holds ((R2 <> R6 & R4 <> R5 & R2 , R4 '||' R4 , R6 & R2 , R5 '||' R5 , R6) implies (ex R8 being (Element of R1) st (ex R9 being (Element of R1) st (R8 <> R9 & R4 , R5 '||' R8 , R9 & R4 , R8 '||' R8 , R5 & R4 , R9 '||' R9 , R5)))))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R5 being (Element of R1);
let R6 being (Element of R1);
assume that
L112: R2 <> R6
and
L113: R4 <> R5
and
L114: R2 , R4 '||' R4 , R6
and
L115: R2 , R5 '||' R5 , R6;
L116: R2 , R5 // R5 , R6 by L112 , L115 , L2;
L117: Mid R2 , R5 , R6 by L116 , AFVECT0:def 3;
L118: R2 , R4 // R4 , R6 by L112 , L114 , L2;
L119: Mid R2 , R4 , R6 by L118 , AFVECT0:def 3;
L120: MDist R4 , R5 by L119 , L113 , L117 , AFVECT0:20;
L121: R4 , R5 // R5 , R4 by L120 , AFVECT0:def 2;
consider R8 being (Element of R1), R9 being (Element of R1) such that L122: R4 , R5 '||' R8 , R9 and L123: (R4 , R8 '||' R8 , R5 & R4 , R9 '||' R9 , R5) by L121 , L7;
L124: (R8 <> R9 implies thesis) by L122 , L123;
thus L125: thesis by L124 , L113 , L122 , L54;
end;
L126: (for R1 being WeakAffVect holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R8 being (Element of R1) holds (for R9 being (Element of R1) holds (for R10 being (Element of R1) holds (for R11 being (Element of R1) holds ((R2 , R4 '||' R8 , R9 & R2 , R6 '||' R10 , R11 & R2 , R8 '||' R8 , R4 & R2 , R10 '||' R10 , R6 & R2 , R9 '||' R9 , R4 & R2 , R11 '||' R11 , R6) implies (ex R12 being (Element of R1) st (ex R13 being (Element of R1) st (R4 , R6 '||' R12 , R13 & R4 , R12 '||' R12 , R6 & R4 , R13 '||' R13 , R6))))))))))))
proof
let R1 being WeakAffVect;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R8 being (Element of R1);
let R9 being (Element of R1);
let R10 being (Element of R1);
let R11 being (Element of R1);
assume L127: (R2 , R4 '||' R8 , R9 & R2 , R6 '||' R10 , R11 & R2 , R8 '||' R8 , R4 & R2 , R10 '||' R10 , R6 & R2 , R9 '||' R9 , R4 & R2 , R11 '||' R11 , R6);
L128: (R2 , R4 // R4 , R2 & R2 , R6 // R6 , R2) by L127 , L7;
L129: R4 , R6 // R6 , R4 by L128 , AFVECT0:12;
thus L130: thesis by L129 , L7;
end;
set D5 = the WeakAffVect;
set D6 = (the carrier of D5);
set D7 = [: D6 , D6 :];
defpred S1[ set , set ] means (ex B1 , B2 , B3 , B4 being (Element of D6) st ($1 = [ B1 , B2 ] & $2 = [ B3 , B4 ] & B1 , B2 '||' B3 , B4));
consider C3 being (Relation of D7 , D7) such that L131: (for B5 , B6 being set holds ([ B5 , B6 ] in C3 iff (B5 in D7 & B6 in D7 & S1[ B5 , B6 ]))) from RELSET_1:sch 1;
L132: (for B7 , B8 , B9 , B10 being (Element of D6) holds ([ [ B7 , B8 ] , [ B9 , B10 ] ] in C3 iff B7 , B8 '||' B9 , B10))
proof
let C4 , C5 , C6 , C7 being (Element of D6);
L133: ([ [ C4 , C5 ] , [ C6 , C7 ] ] in C3 implies C4 , C5 '||' C6 , C7)
proof
assume L134: [ [ C4 , C5 ] , [ C6 , C7 ] ] in C3;
consider C8 , C9 , C10 , C11 being (Element of D6) such that L135: [ C4 , C5 ] = [ C8 , C9 ] and L136: [ C6 , C7 ] = [ C10 , C11 ] and L137: C8 , C9 '||' C10 , C11 by L134 , L131;
L138: C6 = C10 by L136 , XTUPLE_0:1;
L139: (C4 = C8 & C5 = C9) by L135 , XTUPLE_0:1;
thus L140: thesis by L139 , L136 , L137 , L138 , XTUPLE_0:1;
end;
L141: ([ C4 , C5 ] in D7 & [ C6 , C7 ] in D7) by ZFMISC_1:def 2;
thus L142: thesis by L141 , L133 , L131;
end;
set D8 = AffinStruct (# (the carrier of D5) , C3 #);
L143: (for B11 , B12 , B13 , B14 being (Element of D5) holds (for B15 , B16 , B17 , B18 being (Element of D8) holds ((B11 = B15 & B12 = B16 & B13 = B17 & B14 = B18) implies (B11 , B12 '||' B13 , B14 iff B15 , B16 // B17 , B18))))
proof
let C12 , C13 , C14 , C15 being (Element of D5);
let C16 , C17 , C18 , C19 being (Element of D8);
assume that
L144: (C12 = C16 & C13 = C17 & C14 = C18 & C15 = C19);
L145:
now
assume L146: C16 , C17 // C18 , C19;
L147: [ [ C16 , C17 ] , [ C18 , C19 ] ] in C3 by L146 , ANALOAF:def 2;
thus L148: C12 , C13 '||' C14 , C15 by L147 , L144 , L132;
end;
L149:
now
assume L150: C12 , C13 '||' C14 , C15;
L151: [ [ C12 , C13 ] , [ C14 , C15 ] ] in (the CONGR of D8) by L150 , L132;
thus L152: C16 , C17 // C18 , C19 by L151 , L144 , ANALOAF:def 2;
end;
thus L153: thesis by L149 , L145;
end;
L154:
now
thus L155: (ex B19 , B20 being (Element of D8) st B19 <> B20) by STRUCT_0:def 10;
thus L156: (for B21 , B22 being (Element of D8) holds B21 , B22 // B22 , B21)
proof
let C20 , C21 being (Element of D8);
reconsider D9 = C20 , D10 = C21 as (Element of D5);
L157: D9 , D10 '||' D10 , D9 by L51;
thus L158: thesis by L157 , L143;
end;
thus L159: (for B23 , B24 being (Element of D8) holds (B23 , B24 // B23 , B23 implies B23 = B24))
proof
let C22 , C23 being (Element of D8);
assume that
L160: C22 , C23 // C22 , C22;
reconsider D11 = C22 , D12 = C23 as (Element of D5);
L161: D11 , D12 '||' D11 , D11 by L160 , L143;
thus L162: thesis by L161 , L54;
end;
thus L163: (for B25 , B26 , B27 , B28 , B29 , B30 being (Element of D8) holds ((B25 , B26 // B29 , B30 & B27 , B28 // B29 , B30) implies B25 , B26 // B27 , B28))
proof
let C24 , C25 , C26 , C27 , C28 , C29 being (Element of D8);
assume that
L164: (C24 , C25 // C28 , C29 & C26 , C27 // C28 , C29);
reconsider D13 = C24 , D14 = C25 , D15 = C26 , D16 = C27 , D17 = C28 , D18 = C29 as (Element of D5);
L165: (D13 , D14 '||' D17 , D18 & D15 , D16 '||' D17 , D18) by L164 , L143;
L166: D13 , D14 '||' D15 , D16 by L165 , L58;
thus L167: thesis by L166 , L143;
end;
thus L168: (for B31 , B32 being (Element of D8) holds (ex B33 being (Element of D8) st B31 , B33 // B33 , B32))
proof
let C30 , C31 being (Element of D8);
reconsider D19 = C30 , D20 = C31 as (Element of D5);
consider C32 being (Element of D5) such that L169: D19 , C32 '||' C32 , D20 by L64;
reconsider D21 = C32 as (Element of D8);
L170: C30 , D21 // D21 , C31 by L169 , L143;
thus L171: thesis by L170;
end;
thus L172: (for B34 , B35 , B36 , B37 , B38 being (Element of D8) holds ((B34 <> B35 & B36 <> B37 & B38 , B34 // B38 , B35 & B38 , B36 // B38 , B37) implies B34 , B36 // B35 , B37))
proof
let C33 , C34 , C35 , C36 , C37 being (Element of D8);
assume that
L173: (C33 <> C34 & C35 <> C36)
and
L174: (C37 , C33 // C37 , C34 & C37 , C35 // C37 , C36);
reconsider D22 = C33 , D23 = C34 , D24 = C35 , D25 = C36 , D26 = C37 as (Element of D5);
L175: (D26 , D22 '||' D26 , D23 & D26 , D24 '||' D26 , D25) by L174 , L143;
L176: D22 , D24 '||' D23 , D25 by L175 , L173 , L67;
thus L177: thesis by L176 , L143;
end;
thus L178: (for B39 , B40 being (Element of D8) holds (B39 = B40 or (ex B41 being (Element of D8) st ((B39 <> B41 & B39 , B40 // B40 , B41) or (ex B42 , B43 being (Element of D8) st (B42 <> B43 & B39 , B40 // B42 , B43 & B39 , B42 // B42 , B40 & B39 , B43 // B43 , B40))))))
proof
let C38 , C39 being (Element of D8);
assume that
L179: (not C38 = C39);
reconsider D27 = C38 , D28 = C39 as (Element of D5);
L180:
now
given C40 , C41 being (Element of D5) such that
L181: C40 <> C41
and
L182: (D27 , D28 '||' C40 , C41 & D27 , C40 '||' C40 , D28)
and
L183: D27 , C41 '||' C41 , D28;
reconsider D29 = C40 , D30 = C41 as (Element of D8);
L184: C38 , D30 // D30 , C39 by L183 , L143;
L185: (C38 , C39 // D29 , D30 & C38 , D29 // D29 , C39) by L182 , L143;
thus L186: (ex B44 , B45 being (Element of D8) st (B44 <> B45 & C38 , C39 // B44 , B45 & C38 , B44 // B44 , C39 & C38 , B45 // B45 , C39)) by L185 , L181 , L184;
end;
L187:
now
given C42 being (Element of D5) such that
L188: D27 <> C42
and
L189: D27 , D28 '||' D28 , C42;
reconsider D31 = C42 as (Element of D8);
L190: C38 , C39 // C39 , D31 by L189 , L143;
thus L191: (ex B46 being (Element of D8) st (C38 <> B46 & C38 , C39 // C39 , B46)) by L190 , L188;
end;
thus L192: thesis by L187 , L179 , L180 , L78;
end;
thus L193: (for B47 , B48 , B49 , B50 , B51 , B52 being (Element of D8) holds ((B47 , B48 // B48 , B52 & B48 , B49 // B50 , B51 & B48 , B50 // B50 , B49 & B48 , B51 // B51 , B49) implies B47 , B49 // B49 , B52))
proof
let C43 , C44 , C45 , C46 , C47 , C48 being (Element of D8);
assume that
L194: (C43 , C44 // C44 , C48 & C44 , C45 // C46 , C47)
and
L195: (C44 , C46 // C46 , C45 & C44 , C47 // C47 , C45);
reconsider D32 = C43 , D33 = C44 , D34 = C45 , D35 = C46 , D36 = C47 , D37 = C48 as (Element of D5);
L196: (D33 , D35 '||' D35 , D34 & D33 , D36 '||' D36 , D34) by L195 , L143;
L197: (D32 , D33 '||' D33 , D37 & D33 , D34 '||' D35 , D36) by L194 , L143;
L198: D32 , D34 '||' D34 , D37 by L197 , L196 , L91;
thus L199: thesis by L198 , L143;
end;
thus L200: (for B53 , B54 , B55 , B56 being (Element of D8) holds ((B53 <> B56 & B54 <> B55 & B53 , B54 // B54 , B56 & B53 , B55 // B55 , B56) implies (ex B57 , B58 being (Element of D8) st (B57 <> B58 & B54 , B55 // B57 , B58 & B54 , B57 // B57 , B55 & B54 , B58 // B58 , B55))))
proof
let C49 , C50 , C51 , C52 being (Element of D8);
assume that
L201: (C49 <> C52 & C50 <> C51)
and
L202: (C49 , C50 // C50 , C52 & C49 , C51 // C51 , C52);
reconsider D38 = C49 , D39 = C50 , D40 = C51 , D41 = C52 as (Element of D5);
L203: (D38 , D39 '||' D39 , D41 & D38 , D40 '||' D40 , D41) by L202 , L143;
consider C53 , C54 being (Element of D5) such that L204: C53 <> C54 and L205: (D39 , D40 '||' C53 , C54 & D39 , C53 '||' C53 , D40) and L206: D39 , C54 '||' C54 , D40 by L203 , L201 , L111;
reconsider D42 = C53 , D43 = C54 as (Element of D8);
L207: C50 , D43 // D43 , C51 by L206 , L143;
L208: (C50 , C51 // D42 , D43 & C50 , D42 // D42 , C51) by L205 , L143;
thus L209: thesis by L208 , L204 , L207;
end;
thus L210: (for B59 , B60 , B61 , B62 , B63 , B64 , B65 being (Element of D8) holds ((B59 , B60 // B62 , B63 & B59 , B61 // B64 , B65 & B59 , B62 // B62 , B60 & B59 , B64 // B64 , B61 & B59 , B63 // B63 , B60 & B59 , B65 // B65 , B61) implies (ex B66 , B67 being (Element of D8) st (B60 , B61 // B66 , B67 & B60 , B66 // B66 , B61 & B60 , B67 // B67 , B61))))
proof
let C55 , C56 , C57 , C58 , C59 , C60 , C61 being (Element of D8);
assume that
L211: (C55 , C56 // C58 , C59 & C55 , C57 // C60 , C61)
and
L212: (C55 , C58 // C58 , C56 & C55 , C60 // C60 , C57)
and
L213: (C55 , C59 // C59 , C56 & C55 , C61 // C61 , C57);
reconsider D44 = C55 , D45 = C56 , D46 = C57 , D47 = C58 , D48 = C59 , D49 = C60 , D50 = C61 as (Element of D5);
L214: (D44 , D47 '||' D47 , D45 & D44 , D49 '||' D49 , D46) by L212 , L143;
L215: (D44 , D48 '||' D48 , D45 & D44 , D50 '||' D50 , D46) by L213 , L143;
L216: (D44 , D45 '||' D47 , D48 & D44 , D46 '||' D49 , D50) by L211 , L143;
consider C62 , C63 being (Element of D5) such that L217: (D45 , D46 '||' C62 , C63 & D45 , C62 '||' C62 , D46) and L218: D45 , C63 '||' C63 , D46 by L216 , L214 , L215 , L126;
reconsider D51 = C62 , D52 = C63 as (Element of D8);
L219: C56 , D52 // D52 , C57 by L218 , L143;
L220: (C56 , C57 // D51 , D52 & C56 , D51 // D51 , C57) by L217 , L143;
thus L221: thesis by L220 , L219;
end;
end;
definition
let C64 being non empty AffinStruct;
attr C64 is WeakAffSegm-like
means
:L211: ((for B68 , B69 being (Element of C64) holds B68 , B69 // B69 , B68) & (for B70 , B71 being (Element of C64) holds (B70 , B71 // B70 , B70 implies B70 = B71)) & (for B72 , B73 , B74 , B75 , B76 , B77 being (Element of C64) holds ((B72 , B73 // B76 , B77 & B74 , B75 // B76 , B77) implies B72 , B73 // B74 , B75)) & (for B78 , B79 being (Element of C64) holds (ex B80 being (Element of C64) st B78 , B80 // B80 , B79)) & (for B81 , B82 , B83 , B84 , B85 being (Element of C64) holds ((B81 <> B82 & B83 <> B84 & B85 , B81 // B85 , B82 & B85 , B83 // B85 , B84) implies B81 , B83 // B82 , B84)) & (for B86 , B87 being (Element of C64) holds (B86 = B87 or (ex B88 being (Element of C64) st ((B86 <> B88 & B86 , B87 // B87 , B88) or (ex B89 , B90 being (Element of C64) st (B89 <> B90 & B86 , B87 // B89 , B90 & B86 , B89 // B89 , B87 & B86 , B90 // B90 , B87)))))) & (for B91 , B92 , B93 , B94 , B95 , B96 being (Element of C64) holds ((B91 , B92 // B92 , B96 & B92 , B93 // B94 , B95 & B92 , B94 // B94 , B93 & B92 , B95 // B95 , B93) implies B91 , B93 // B93 , B96)) & (for B97 , B98 , B99 , B100 being (Element of C64) holds ((B97 <> B100 & B98 <> B99 & B97 , B98 // B98 , B100 & B97 , B99 // B99 , B100) implies (ex B101 , B102 being (Element of C64) st (B101 <> B102 & B98 , B99 // B101 , B102 & B98 , B101 // B101 , B99 & B98 , B102 // B102 , B99)))) & (for B103 , B104 , B105 , B106 , B107 , B108 , B109 being (Element of C64) holds ((B103 , B104 // B106 , B107 & B103 , B105 // B108 , B109 & B103 , B106 // B106 , B104 & B103 , B108 // B108 , B105 & B103 , B107 // B107 , B104 & B103 , B109 // B109 , B105) implies (ex B110 , B111 being (Element of C64) st (B104 , B105 // B110 , B111 & B104 , B110 // B110 , B105 & B104 , B111 // B111 , B105)))));
end;
registration
cluster strict WeakAffSegm-like for non trivial non trivial non trivial non trivial AffinStruct;
existence
proof
L213: D8 is WeakAffSegm-like non trivial by L211 , L154;
thus L214: thesis by L213;
end;
end;
definition
mode WeakAffSegm
is WeakAffSegm-like non trivial AffinStruct;
end;
theorem
L217: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds R15 , R16 // R15 , R16)))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
L218: R15 , R16 // R16 , R15 by L211;
thus L219: thesis by L218 , L211;
end;
theorem
L220: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds (for R19 being (Element of R14) holds (for R20 being (Element of R14) holds (R15 , R16 // R19 , R20 implies R19 , R20 // R15 , R16))))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R19 being (Element of R14);
let R20 being (Element of R14);
assume L221: R15 , R16 // R19 , R20;
L222: R19 , R20 // R19 , R20 by L217;
thus L223: thesis by L222 , L221 , L211;
end;
theorem
L224: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds (for R19 being (Element of R14) holds (for R20 being (Element of R14) holds (R15 , R16 // R19 , R20 implies R15 , R16 // R20 , R19))))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R19 being (Element of R14);
let R20 being (Element of R14);
assume L225: R15 , R16 // R19 , R20;
L226: R20 , R19 // R19 , R20 by L211;
thus L227: thesis by L226 , L225 , L211;
end;
theorem
L228: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds (for R19 being (Element of R14) holds (for R20 being (Element of R14) holds (R15 , R16 // R19 , R20 implies R16 , R15 // R19 , R20))))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R19 being (Element of R14);
let R20 being (Element of R14);
assume L229: R15 , R16 // R19 , R20;
L230: R19 , R20 // R15 , R16 by L229 , L220;
L231: R19 , R20 // R16 , R15 by L230 , L224;
thus L232: thesis by L231 , L220;
end;
theorem
L233: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds R15 , R15 // R16 , R16)))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
L234:
now
consider R19 being (Element of R14) such that L235: R15 , R19 // R19 , R16 by L211;
assume L236: R15 <> R16;
L237: R19 , R15 // R19 , R16 by L235 , L228;
thus L238: thesis by L237 , L236 , L211;
end;
thus L239: thesis by L234 , L211;
end;
theorem
L240: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds (for R19 being (Element of R14) holds (R15 , R16 // R19 , R19 implies R15 = R16)))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R19 being (Element of R14);
assume L241: R15 , R16 // R19 , R19;
L242: R15 , R15 // R19 , R19 by L233;
L243: R15 , R16 // R15 , R15 by L242 , L241 , L211;
thus L244: thesis by L243 , L211;
end;
theorem
L245: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds (for R19 being (Element of R14) holds (for R21 being (Element of R14) holds (for R22 being (Element of R14) holds ((R15 , R16 // R21 , R22 & R15 , R16 // R16 , R19 & R15 , R21 // R21 , R16 & R15 , R22 // R22 , R16) implies R15 = R19)))))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R19 being (Element of R14);
let R21 being (Element of R14);
let R22 being (Element of R14);
assume that
L246: R15 , R16 // R21 , R22
and
L247: R15 , R16 // R16 , R19
and
L248: R15 , R21 // R21 , R16
and
L249: R15 , R22 // R22 , R16;
L250: R21 , R16 // R15 , R21 by L248 , L220;
L251: R21 , R16 // R21 , R15 by L250 , L224;
L252: R16 , R21 // R21 , R15 by L251 , L228;
L253: R22 , R16 // R15 , R22 by L249 , L220;
L254: R22 , R16 // R22 , R15 by L253 , L224;
L255: R16 , R22 // R22 , R15 by L254 , L228;
L256: R16 , R15 // R21 , R22 by L246 , L228;
L257: R15 , R15 // R15 , R19 by L256 , L247 , L252 , L255 , L211;
L258: R15 , R19 // R15 , R15 by L257 , L220;
thus L259: thesis by L258 , L211;
end;
theorem
L260: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds (for R17 being (Element of R14) holds (for R18 being (Element of R14) holds ((R15 , R17 // R15 , R18 & R15 , R16 // R15 , R18) implies (R16 = R17 or R16 = R18 or R17 = R18)))))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R17 being (Element of R14);
let R18 being (Element of R14);
assume L261: (R15 , R17 // R15 , R18 & R15 , R16 // R15 , R18);
L262:
now
assume L263: (R17 <> R18 & R16 <> R18);
L264: R17 , R16 // R18 , R18 by L263 , L261 , L211;
thus L265: thesis by L264 , L240;
end;
thus L266: thesis by L262;
end;
definition
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
pred MDist R15 , R16
means
:L267: (ex R21 being (Element of R14) st (ex R22 being (Element of R14) st (R21 <> R22 & R15 , R16 // R21 , R22 & R15 , R21 // R21 , R16 & R15 , R22 // R22 , R16)))
;end;
definition
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R19 being (Element of R14);
pred Mid R15 , R16 , R19
means
((R15 = R16 & R16 = R19 & R15 = R19) or (R15 = R19 & MDist R15 , R16) or (R15 <> R19 & R15 , R16 // R16 , R19))
;end;
theorem
L270: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds ((R15 <> R16 & (not MDist R15 , R16)) implies (ex R19 being (Element of R14) st (R15 <> R19 & R15 , R16 // R16 , R19))))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
assume L271: (R15 <> R16 & (not MDist R15 , R16));
L272: (R15 = R16 or (ex R19 being (Element of R14) st ((R15 <> R19 & R15 , R16 // R16 , R19) or (ex R21 being (Element of R14) st (ex R22 being (Element of R14) st (R21 <> R22 & R15 , R16 // R21 , R22 & R15 , R21 // R21 , R16 & R15 , R22 // R22 , R16)))))) by L211;
thus L273: thesis by L272 , L271 , L267;
end;
theorem
L274: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds (for R19 being (Element of R14) holds (( MDist R15 , R16 & R15 , R16 // R16 , R19) implies R15 = R19)))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
let R19 being (Element of R14);
assume that
L275: MDist R15 , R16
and
L276: R15 , R16 // R16 , R19;
L277: (ex R21 being (Element of R14) st (ex R22 being (Element of R14) st (R21 <> R22 & R15 , R16 // R21 , R22 & R15 , R21 // R21 , R16 & R15 , R22 // R22 , R16))) by L275 , L267;
thus L278: thesis by L277 , L276 , L245;
end;
theorem
L279: (for R14 being WeakAffSegm holds (for R15 being (Element of R14) holds (for R16 being (Element of R14) holds ( MDist R15 , R16 implies R15 <> R16))))
proof
let R14 being WeakAffSegm;
let R15 being (Element of R14);
let R16 being (Element of R14);
assume L280: MDist R15 , R16;
L281: (ex R21 being (Element of R14) st (ex R22 being (Element of R14) st (R21 <> R22 & R15 , R16 // R21 , R22 & R15 , R21 // R21 , R16 & R15 , R22 // R22 , R16))) by L280 , L267;
thus L282: thesis by L281 , L220 , L240;
end;