/
aff_2.miz
2549 lines (2539 loc) · 97.3 KB
/
aff_2.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
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
:: Classical Configurations in Affine Planes
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received April 13, 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 DIRAF, SUBSET_1, AFF_1, ANALOAF, INCSP_1, AFF_2;
notations STRUCT_0, ANALOAF, DIRAF, AFF_1;
constructors AFF_1;
registrations STRUCT_0;
theorems AFF_1;
begin
definition
let R1 being AffinPlane;
attr R1 is satisfying_PPAP
means
:L1: (for R20 being (Subset of R1) holds (for R21 being (Subset of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R20 is being_line & R21 is being_line & R2 in R20 & R4 in R20 & R6 in R20 & R3 in R21 & R5 in R21 & R7 in R21 & R2 , R5 // R4 , R3 & R4 , R7 // R6 , R5) implies R2 , R7 // R6 , R3)))))))));
end;
definition
let C1 being AffinSpace;
attr C1 is Pappian
means
:L3: (for B1 , B2 being (Subset of C1) holds (for B3 , B4 , B5 , B6 , B7 , B8 , B9 being (Element of C1) holds ((B1 is being_line & B2 is being_line & B1 <> B2 & B3 in B1 & B3 in B2 & B3 <> B4 & B3 <> B7 & B3 <> B5 & B3 <> B8 & B3 <> B6 & B3 <> B9 & B4 in B1 & B5 in B1 & B6 in B1 & B7 in B2 & B8 in B2 & B9 in B2 & B4 , B8 // B5 , B7 & B5 , B9 // B6 , B8) implies B4 , B9 // B6 , B7)));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_PAP_1
means
:L5: (for R20 being (Subset of R1) holds (for R21 being (Subset of R1) holds (for R10 being (Element of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R20 is being_line & R21 is being_line & R20 <> R21 & R10 in R20 & R10 in R21 & R10 <> R2 & R10 <> R3 & R10 <> R4 & R10 <> R5 & R10 <> R6 & R10 <> R7 & R2 in R20 & R4 in R20 & R6 in R20 & R5 in R21 & R7 in R21 & R2 , R5 // R4 , R3 & R4 , R7 // R6 , R5 & R2 , R7 // R6 , R3 & R4 <> R6) implies R3 in R21))))))))));
end;
definition
let C2 being AffinSpace;
attr C2 is Desarguesian
means
:L7: (for B10 , B11 , B12 being (Subset of C2) holds (for B13 , B14 , B15 , B16 , B17 , B18 , B19 being (Element of C2) holds ((B13 in B10 & B13 in B11 & B13 in B12 & B13 <> B14 & B13 <> B15 & B13 <> B16 & B14 in B10 & B17 in B10 & B15 in B11 & B18 in B11 & B16 in B12 & B19 in B12 & B10 is being_line & B11 is being_line & B12 is being_line & B10 <> B11 & B10 <> B12 & B14 , B15 // B17 , B18 & B14 , B16 // B17 , B19) implies B15 , B16 // B18 , B19)));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_DES_1
means
:L9: (for R15 being (Subset of R1) holds (for R22 being (Subset of R1) holds (for R16 being (Subset of R1) holds (for R10 being (Element of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R10 in R15 & R10 in R22 & R10 <> R2 & R10 <> R4 & R10 <> R6 & R2 in R15 & R3 in R15 & R4 in R22 & R5 in R22 & R6 in R16 & R7 in R16 & R15 is being_line & R22 is being_line & R16 is being_line & R15 <> R22 & R15 <> R16 & R2 , R4 // R3 , R5 & R2 , R6 // R3 , R7 & R4 , R6 // R5 , R7 & (not LIN R2 , R4 , R6) & R6 <> R7) implies R10 in R16)))))))))));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_DES_2
means
(for R15 being (Subset of R1) holds (for R22 being (Subset of R1) holds (for R16 being (Subset of R1) holds (for R10 being (Element of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R10 in R15 & R10 in R22 & R10 in R16 & R10 <> R2 & R10 <> R4 & R10 <> R6 & R2 in R15 & R3 in R15 & R4 in R22 & R5 in R22 & R6 in R16 & R15 is being_line & R22 is being_line & R16 is being_line & R15 <> R22 & R15 <> R16 & R2 , R4 // R3 , R5 & R2 , R6 // R3 , R7 & R4 , R6 // R5 , R7) implies R7 in R16)))))))))));
end;
definition
let C3 being AffinSpace;
attr C3 is Moufangian
means
:L12: (for B20 being (Subset of C3) holds (for B21 , B22 , B23 , B24 , B25 , B26 , B27 being (Element of C3) holds ((B20 is being_line & B21 in B20 & B24 in B20 & B27 in B20 & (not B22 in B20) & B21 <> B24 & B22 <> B23 & LIN B21 , B22 , B25 & LIN B21 , B23 , B26 & B22 , B23 // B25 , B26 & B22 , B24 // B25 , B27 & B22 , B23 // B20) implies B23 , B24 // B26 , B27)));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_TDES_1
means
:L14: (for R19 being (Subset of R1) holds (for R10 being (Element of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R19 is being_line & R10 in R19 & R6 in R19 & R7 in R19 & (not R2 in R19) & R10 <> R6 & R2 <> R4 & LIN R10 , R2 , R3 & R2 , R4 // R3 , R5 & R4 , R6 // R5 , R7 & R2 , R6 // R3 , R7 & R2 , R4 // R19) implies LIN R10 , R4 , R5)))))))));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_TDES_2
means
:L16: (for R19 being (Subset of R1) holds (for R10 being (Element of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R19 is being_line & R10 in R19 & R6 in R19 & R7 in R19 & (not R2 in R19) & R10 <> R6 & R2 <> R4 & LIN R10 , R2 , R3 & LIN R10 , R4 , R5 & R4 , R6 // R5 , R7 & R2 , R6 // R3 , R7 & R2 , R4 // R19) implies R2 , R4 // R3 , R5)))))))));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_TDES_3
means
:L18: (for R19 being (Subset of R1) holds (for R10 being (Element of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R19 is being_line & R10 in R19 & R6 in R19 & (not R2 in R19) & R10 <> R6 & R2 <> R4 & LIN R10 , R2 , R3 & LIN R10 , R4 , R5 & R2 , R4 // R3 , R5 & R2 , R6 // R3 , R7 & R4 , R6 // R5 , R7 & R2 , R4 // R19) implies R7 in R19)))))))));
end;
definition
let C4 being AffinSpace;
attr C4 is translational
means
:L20: (for B28 , B29 , B30 being (Subset of C4) holds (for B31 , B32 , B33 , B34 , B35 , B36 being (Element of C4) holds ((B28 // B29 & B28 // B30 & B31 in B28 & B34 in B28 & B32 in B29 & B35 in B29 & B33 in B30 & B36 in B30 & B28 is being_line & B29 is being_line & B30 is being_line & B28 <> B29 & B28 <> B30 & B31 , B32 // B34 , B35 & B31 , B33 // B34 , B36) implies B32 , B33 // B35 , B36)));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_des_1
means
:L22: (for R15 being (Subset of R1) holds (for R22 being (Subset of R1) holds (for R16 being (Subset of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R15 // R22 & R2 in R15 & R3 in R15 & R4 in R22 & R5 in R22 & R6 in R16 & R7 in R16 & R15 is being_line & R22 is being_line & R16 is being_line & R15 <> R22 & R15 <> R16 & R2 , R4 // R3 , R5 & R2 , R6 // R3 , R7 & R4 , R6 // R5 , R7 & (not LIN R2 , R4 , R6) & R6 <> R7) implies R15 // R16))))))))));
end;
definition
let C5 being AffinSpace;
attr C5 is satisfying_pap
means
:L24: (for B37 , B38 being (Subset of C5) holds (for B39 , B40 , B41 , B42 , B43 , B44 being (Element of C5) holds ((B37 is being_line & B38 is being_line & B39 in B37 & B40 in B37 & B41 in B37 & B37 // B38 & B37 <> B38 & B42 in B38 & B43 in B38 & B44 in B38 & B39 , B43 // B40 , B42 & B40 , B44 // B41 , B43) implies B39 , B44 // B41 , B42)));
end;
definition
let R1 being AffinPlane;
attr R1 is satisfying_pap_1
means
:L26: (for R20 being (Subset of R1) holds (for R21 being (Subset of R1) holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds (for R3 being (Element of R1) holds (for R5 being (Element of R1) holds (for R7 being (Element of R1) holds ((R20 is being_line & R21 is being_line & R2 in R20 & R4 in R20 & R6 in R20 & R20 // R21 & R20 <> R21 & R3 in R21 & R5 in R21 & R2 , R5 // R4 , R3 & R4 , R7 // R6 , R5 & R2 , R7 // R6 , R3 & R3 <> R5) implies R7 in R21)))))))));
end;
theorem
L28: (for R1 being AffinPlane holds (R1 is Pappian iff R1 is satisfying_PAP_1))
proof
let R1 being AffinPlane;
thus L29:now
assume L30: R1 is Pappian;
thus L31: R1 is satisfying_PAP_1
proof
let R20 being (Subset of R1);
let R21 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L32: R20 is being_line
and
L33: R21 is being_line
and
L34: R20 <> R21
and
L35: R10 in R20
and
L36: R10 in R21
and
L37: R10 <> R2
and
L38: R10 <> R3
and
L39: R10 <> R4
and
L40: R10 <> R5
and
L41: R10 <> R6
and
L42: R10 <> R7
and
L43: R2 in R20
and
L44: R4 in R20
and
L45: R6 in R20
and
L46: R5 in R21
and
L47: R7 in R21
and
L48: R2 , R5 // R4 , R3
and
L49: R4 , R7 // R6 , R5
and
L50: R2 , R7 // R6 , R3
and
L51: R4 <> R6;
L52: R2 <> R7 by L32 , L33 , L34 , L35 , L36 , L37 , L43 , L47 , AFF_1:18;
L53: R4 <> R3
proof
assume L54: R4 = R3;
L55: R6 , R4 // R2 , R7 by L54 , L50 , AFF_1:4;
L56: R7 in R20 by L55 , L32 , L43 , L44 , L45 , L51 , AFF_1:48;
thus L57: contradiction by L56 , L32 , L33 , L34 , L35 , L36 , L42 , L47 , AFF_1:18;
end;
L58: (not R4 , R3 // R21)
proof
assume L59: R4 , R3 // R21;
L60: R4 , R3 // R2 , R5 by L48 , AFF_1:4;
L61: R2 , R5 // R21 by L60 , L53 , L59 , AFF_1:32;
L62: R5 , R2 // R21 by L61 , AFF_1:34;
L63: R2 in R21 by L62 , L33 , L46 , AFF_1:23;
thus L64: contradiction by L63 , L32 , L33 , L34 , L35 , L36 , L37 , L43 , AFF_1:18;
end;
consider R8 being (Element of R1) such that L65: R8 in R21 and L66: LIN R4 , R3 , R8 by L58 , L33 , AFF_1:59;
L67: R4 , R3 // R4 , R8 by L66 , AFF_1:def 1;
L68: R10 <> R8
proof
assume L69: R10 = R8;
L70: R4 , R10 // R2 , R5 by L69 , L48 , L53 , L67 , AFF_1:5;
L71: R5 in R20 by L70 , L32 , L35 , L39 , L43 , L44 , AFF_1:48;
thus L72: contradiction by L71 , L32 , L33 , L34 , L35 , L36 , L40 , L46 , AFF_1:18;
end;
L73: R2 , R5 // R4 , R8 by L48 , L53 , L67 , AFF_1:5;
L74: R2 , R7 // R6 , R8 by L73 , L30 , L32 , L33 , L34 , L35 , L36 , L37 , L39 , L40 , L41 , L42 , L43 , L44 , L45 , L46 , L47 , L49 , L65 , L68 , L3;
L75: R6 , R3 // R6 , R8 by L74 , L50 , L52 , AFF_1:5;
L76: LIN R6 , R3 , R8 by L75 , AFF_1:def 1;
L77: LIN R3 , R8 , R6 by L76 , AFF_1:6;
L78: LIN R3 , R8 , R8 by AFF_1:7;
assume L79: (not R3 in R21);
L80: LIN R3 , R8 , R4 by L66 , AFF_1:6;
L81: R8 in R20 by L80 , L32 , L44 , L45 , L51 , L79 , L65 , L77 , L78 , AFF_1:8 , AFF_1:25;
thus L82: contradiction by L81 , L32 , L33 , L34 , L35 , L36 , L65 , L68 , AFF_1:18;
end;
end;
assume L32: R1 is satisfying_PAP_1;
let R20 being (Subset of R1);
let R21 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L33: R20 is being_line
and
L34: R21 is being_line
and
L35: (R20 <> R21 & R10 in R20 & R10 in R21)
and
L36: R10 <> R2
and
L37: R10 <> R3
and
L38: R10 <> R4
and
L39: R10 <> R5
and
L40: (R10 <> R6 & R10 <> R7)
and
L41: R2 in R20
and
L42: R4 in R20
and
L43: R6 in R20
and
L44: R3 in R21
and
L45: R5 in R21
and
L46: R7 in R21
and
L47: R2 , R5 // R4 , R3
and
L48: R4 , R7 // R6 , R5;
set D1 = ( Line (R2 , R7) );
set D2 = ( Line (R4 , R3) );
L49: R4 <> R3 by L33 , L34 , L35 , L37 , L42 , L44 , AFF_1:18;
L50: R4 in D2 by L49 , AFF_1:24;
assume L51: (not R2 , R7 // R6 , R3);
L52: R2 <> R7 by L51 , AFF_1:3;
L53: (R2 in D1 & R7 in D1) by L52 , AFF_1:24;
L54: R3 in D2 by L49 , AFF_1:24;
L55: D1 is being_line by L52 , AFF_1:24;
consider R19 being (Subset of R1) such that L56: R6 in R19 and L57: D1 // R19 by L55 , AFF_1:49;
L58: R4 <> R6
proof
assume L59: R4 = R6;
L60: LIN R4 , R7 , R5 by L59 , L48 , AFF_1:def 1;
L61: LIN R5 , R7 , R4 by L60 , AFF_1:6;
L62: (R5 = R7 or R4 in R21) by L61 , L34 , L45 , L46 , AFF_1:25;
thus L63: contradiction by L62 , L33 , L34 , L35 , L38 , L42 , L47 , L51 , L59 , AFF_1:18;
end;
L64: R5 <> R7
proof
assume L65: R5 = R7;
L66: R5 , R4 // R5 , R6 by L65 , L48 , AFF_1:4;
L67: LIN R5 , R4 , R6 by L66 , AFF_1:def 1;
L68: LIN R4 , R6 , R5 by L67 , AFF_1:6;
L69: R5 in R20 by L68 , L33 , L42 , L43 , L58 , AFF_1:25;
thus L70: contradiction by L69 , L33 , L34 , L35 , L39 , L45 , AFF_1:18;
end;
L71: (not D2 // R19)
proof
assume L72: D2 // R19;
L73: D2 // D1 by L72 , L57 , AFF_1:44;
L74: R4 , R3 // R2 , R7 by L73 , L53 , L50 , L54 , AFF_1:39;
L75: R2 , R5 // R2 , R7 by L74 , L47 , L49 , AFF_1:5;
L76: LIN R2 , R5 , R7 by L75 , AFF_1:def 1;
L77: LIN R5 , R7 , R2 by L76 , AFF_1:6;
L78: R2 in R21 by L77 , L34 , L45 , L46 , L64 , AFF_1:25;
thus L79: contradiction by L78 , L33 , L34 , L35 , L36 , L41 , AFF_1:18;
end;
L80: D2 is being_line by L49 , AFF_1:24;
L81: R19 is being_line by L57 , AFF_1:36;
consider R8 being (Element of R1) such that L82: R8 in D2 and L83: R8 in R19 by L81 , L80 , L71 , AFF_1:58;
L84: R2 , R7 // R6 , R8 by L53 , L56 , L57 , L83 , AFF_1:39;
L85: LIN R4 , R8 , R3 by L80 , L50 , L54 , L82 , AFF_1:21;
L86: R4 , R8 // R4 , R3 by L85 , AFF_1:def 1;
L87: R2 , R5 // R4 , R8 by L86 , L47 , L49 , AFF_1:5;
L88: R8 in R21 by L87 , L32 , L33 , L34 , L35 , L36 , L38 , L39 , L40 , L41 , L42 , L43 , L45 , L46 , L48 , L58 , L84 , L5;
L89: R21 = D2 by L88 , L34 , L44 , L51 , L80 , L54 , L82 , L84 , AFF_1:18;
thus L90: contradiction by L89 , L33 , L34 , L35 , L38 , L42 , L50 , AFF_1:18;
end;
theorem
L91: (for R1 being AffinPlane holds (R1 is Desarguesian iff R1 is satisfying_DES_1))
proof
let R1 being AffinPlane;
thus L92:now
assume L93: R1 is Desarguesian;
thus L94: R1 is satisfying_DES_1
proof
let R15 being (Subset of R1);
let R22 being (Subset of R1);
let R16 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L95: R10 in R15
and
L96: R10 in R22
and
L97: R10 <> R2
and
L98: R10 <> R4
and
L99: R10 <> R6
and
L100: R2 in R15
and
L101: R3 in R15
and
L102: R4 in R22
and
L103: R5 in R22
and
L104: R6 in R16
and
L105: R7 in R16
and
L106: R15 is being_line
and
L107: R22 is being_line
and
L108: R16 is being_line
and
L109: R15 <> R22
and
L110: R15 <> R16
and
L111: R2 , R4 // R3 , R5
and
L112: R2 , R6 // R3 , R7
and
L113: R4 , R6 // R5 , R7
and
L114: (not LIN R2 , R4 , R6)
and
L115: R6 <> R7;
set D3 = ( Line (R10 , R7) );
assume L116: (not R10 in R16);
L117: D3 is being_line by L116 , L105 , AFF_1:24;
L118: R3 <> R7
proof
assume L119: R3 = R7;
L120: R4 , R6 // R3 , R5 by L119 , L113 , AFF_1:4;
L121: (R2 , R4 // R4 , R6 or R3 = R5) by L120 , L111 , AFF_1:5;
L122: (R4 , R2 // R4 , R6 or R3 = R5) by L121 , AFF_1:4;
L123: ( LIN R4 , R2 , R6 or R3 = R5) by L122 , AFF_1:def 1;
thus L124: contradiction by L123 , L95 , L96 , L101 , L103 , L105 , L106 , L107 , L109 , L114 , L116 , L119 , AFF_1:6 , AFF_1:18;
end;
L125: R15 <> D3
proof
assume L126: R15 = D3;
L127: R7 in R15 by L126 , L95 , AFF_1:24;
L128: R3 , R7 // R2 , R6 by L112 , AFF_1:4;
L129: R6 in R15 by L128 , L100 , L101 , L106 , L118 , L127 , AFF_1:48;
thus L130: contradiction by L129 , L104 , L105 , L106 , L108 , L110 , L115 , L127 , AFF_1:18;
end;
L131: R2 <> R6 by L114 , AFF_1:7;
L132: R10 in D3 by L105 , L116 , AFF_1:24;
L133: R7 in D3 by L105 , L116 , AFF_1:24;
L134: (not R2 , R6 // D3)
proof
assume L135: R2 , R6 // D3;
L136: R3 , R7 // D3 by L135 , L112 , L131 , AFF_1:32;
L137: R7 , R3 // D3 by L136 , AFF_1:34;
L138: R3 in D3 by L137 , L117 , L133 , AFF_1:23;
L139: R3 in R22 by L138 , L95 , L96 , L101 , L106 , L117 , L132 , L125 , AFF_1:18;
L140: R3 , R5 // R4 , R2 by L111 , AFF_1:4;
L141: (R3 = R5 or R2 in R22) by L140 , L102 , L103 , L107 , L139 , AFF_1:48;
L142: R2 , R6 // R4 , R6 by L141 , L95 , L96 , L97 , L100 , L106 , L107 , L109 , L112 , L113 , L118 , AFF_1:5 , AFF_1:18;
L143: R6 , R2 // R6 , R4 by L142 , AFF_1:4;
L144: LIN R6 , R2 , R4 by L143 , AFF_1:def 1;
thus L145: contradiction by L144 , L114 , AFF_1:6;
end;
consider R8 being (Element of R1) such that L146: R8 in D3 and L147: LIN R2 , R6 , R8 by L134 , L117 , AFF_1:59;
L148: R10 <> R8
proof
assume L149: R10 = R8;
L150: LIN R2 , R10 , R6 by L149 , L147 , AFF_1:6;
L151: R6 in R15 by L150 , L95 , L97 , L100 , L106 , AFF_1:25;
L152: R7 in R15 by L151 , L100 , L101 , L106 , L112 , L131 , AFF_1:48;
thus L153: contradiction by L152 , L104 , L105 , L106 , L108 , L110 , L115 , L151 , AFF_1:18;
end;
L154: R5 <> R7
proof
assume L155: R5 = R7;
L156: (R3 = R5 or R2 , R6 // R2 , R4) by L155 , L111 , L112 , AFF_1:5;
L157: (R3 = R5 or LIN R2 , R6 , R4) by L156 , AFF_1:def 1;
L158: R4 , R6 // R2 , R6 by L157 , L112 , L113 , L114 , L118 , AFF_1:5 , AFF_1:6;
L159: R6 , R4 // R6 , R2 by L158 , AFF_1:4;
L160: LIN R6 , R4 , R2 by L159 , AFF_1:def 1;
thus L161: contradiction by L160 , L114 , AFF_1:6;
end;
L162: R2 , R6 // R2 , R8 by L147 , AFF_1:def 1;
L163: R2 , R8 // R3 , R7 by L162 , L112 , L131 , AFF_1:5;
L164: R4 , R8 // R5 , R7 by L163 , L93 , L95 , L96 , L97 , L98 , L100 , L101 , L102 , L103 , L106 , L107 , L109 , L111 , L117 , L132 , L133 , L125 , L146 , L148 , L7;
L165: R4 , R8 // R4 , R6 by L164 , L113 , L154 , AFF_1:5;
L166: (not LIN R2 , R4 , R8)
proof
assume L167: LIN R2 , R4 , R8;
L168: R2 , R4 // R2 , R8 by L167 , AFF_1:def 1;
L169: (R2 , R4 // R2 , R6 or R2 = R8) by L168 , L162 , AFF_1:5;
thus L170: contradiction by L169 , L95 , L97 , L100 , L106 , L114 , L117 , L132 , L125 , L146 , AFF_1:18 , AFF_1:def 1;
end;
L171: LIN R2 , R8 , R6 by L147 , AFF_1:6;
L172: R6 in D3 by L171 , L146 , L166 , L165 , AFF_1:14;
thus L173: contradiction by L172 , L104 , L105 , L108 , L115 , L116 , L117 , L132 , L133 , AFF_1:18;
end;
end;
assume L95: R1 is satisfying_DES_1;
let R15 being (Subset of R1);
let R22 being (Subset of R1);
let R16 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L96: R10 in R15
and
L97: R10 in R22
and
L98: R10 in R16
and
L99: R10 <> R2
and
L100: R10 <> R4
and
L101: R10 <> R6
and
L102: R2 in R15
and
L103: R3 in R15
and
L104: R4 in R22
and
L105: R5 in R22
and
L106: R6 in R16
and
L107: R7 in R16
and
L108: R15 is being_line
and
L109: R22 is being_line
and
L110: R16 is being_line
and
L111: R15 <> R22
and
L112: R15 <> R16
and
L113: R2 , R4 // R3 , R5
and
L114: R2 , R6 // R3 , R7;
assume L115: (not R4 , R6 // R5 , R7);
L116: R3 <> R5
proof
L117: R3 , R7 // R6 , R2 by L114 , AFF_1:4;
assume L118: R3 = R5;
L119: R3 in R16 by L118 , L96 , L97 , L98 , L103 , L105 , L108 , L109 , L111 , AFF_1:18;
L120: (R2 in R16 or R3 = R7) by L119 , L106 , L107 , L110 , L117 , AFF_1:48;
thus L121: contradiction by L120 , L96 , L98 , L99 , L102 , L108 , L110 , L112 , L115 , L118 , AFF_1:3 , AFF_1:18;
end;
L122: R3 <> R7
proof
assume L123: R3 = R7;
L124: R3 in R22 by L123 , L96 , L97 , L98 , L103 , L107 , L108 , L110 , L112 , AFF_1:18;
L125: R3 , R5 // R4 , R2 by L113 , AFF_1:4;
L126: R2 in R22 by L125 , L104 , L105 , L109 , L116 , L124 , AFF_1:48;
thus L127: contradiction by L126 , L96 , L97 , L99 , L102 , L108 , L109 , L111 , AFF_1:18;
end;
L128: R10 <> R7
proof
assume L129: R10 = R7;
L130: R3 , R7 // R2 , R6 by L114 , AFF_1:4;
L131: R6 in R15 by L130 , L96 , L102 , L103 , L108 , L122 , L129 , AFF_1:48;
thus L132: contradiction by L131 , L96 , L98 , L101 , L106 , L108 , L110 , L112 , AFF_1:18;
end;
set D4 = ( Line (R2 , R6) );
set D5 = ( Line (R5 , R7) );
L133: R2 <> R6 by L96 , L98 , L99 , L102 , L106 , L108 , L110 , L112 , AFF_1:18;
L134: R6 in D4 by L133 , AFF_1:24;
L135: R2 <> R4 by L96 , L97 , L99 , L102 , L104 , L108 , L109 , L111 , AFF_1:18;
L136: (not LIN R3 , R5 , R7)
proof
assume L137: LIN R3 , R5 , R7;
L138: R3 , R5 // R3 , R7 by L137 , AFF_1:def 1;
L139: R3 , R5 // R2 , R6 by L138 , L114 , L122 , AFF_1:5;
L140: R2 , R4 // R2 , R6 by L139 , L113 , L116 , AFF_1:5;
L141: LIN R2 , R4 , R6 by L140 , AFF_1:def 1;
L142: LIN R4 , R6 , R2 by L141 , AFF_1:6;
L143: R4 , R6 // R4 , R2 by L142 , AFF_1:def 1;
L144: R4 , R6 // R2 , R4 by L143 , AFF_1:4;
L145: R4 , R6 // R3 , R5 by L144 , L113 , L135 , AFF_1:5;
L146: LIN R5 , R7 , R3 by L137 , AFF_1:6;
L147: R5 , R7 // R5 , R3 by L146 , AFF_1:def 1;
L148: R5 , R7 // R3 , R5 by L147 , AFF_1:4;
thus L149: contradiction by L148 , L115 , L116 , L145 , AFF_1:5;
end;
L150: R5 <> R7 by L115 , AFF_1:3;
L151: (R5 in D5 & R7 in D5) by L150 , AFF_1:24;
L152: D5 is being_line by L150 , AFF_1:24;
consider R18 being (Subset of R1) such that L153: R4 in R18 and L154: D5 // R18 by L152 , AFF_1:49;
L155: R2 in D4 by L133 , AFF_1:24;
L156: (not D4 // R18)
proof
assume L157: D4 // R18;
L158: D4 // D5 by L157 , L154 , AFF_1:44;
L159: R2 , R6 // R5 , R7 by L158 , L155 , L134 , L151 , AFF_1:39;
L160: R3 , R7 // R5 , R7 by L159 , L114 , L133 , AFF_1:5;
L161: R7 , R3 // R7 , R5 by L160 , AFF_1:4;
L162: LIN R7 , R3 , R5 by L161 , AFF_1:def 1;
thus L163: contradiction by L162 , L136 , AFF_1:6;
end;
L164: D4 is being_line by L133 , AFF_1:24;
L165: R18 is being_line by L154 , AFF_1:36;
consider R8 being (Element of R1) such that L166: R8 in D4 and L167: R8 in R18 by L165 , L164 , L156 , AFF_1:58;
L168: LIN R2 , R6 , R8 by L164 , L155 , L134 , L166 , AFF_1:21;
L169: R2 , R6 // R2 , R8 by L168 , AFF_1:def 1;
L170: R2 , R8 // R3 , R7 by L169 , L114 , L133 , AFF_1:5;
set D6 = ( Line (R7 , R8) );
L171: R2 <> R3
proof
assume L172: R2 = R3;
L173: LIN R2 , R6 , R7 by L172 , L114 , AFF_1:def 1;
L174: LIN R6 , R7 , R2 by L173 , AFF_1:6;
L175: (R6 = R7 or R2 in R16) by L174 , L106 , L107 , L110 , AFF_1:25;
L176: LIN R2 , R4 , R5 by L113 , L172 , AFF_1:def 1;
L177: LIN R4 , R5 , R2 by L176 , AFF_1:6;
L178: (R4 = R5 or R2 in R22) by L177 , L104 , L105 , L109 , AFF_1:25;
thus L179: contradiction by L178 , L96 , L97 , L98 , L99 , L102 , L108 , L109 , L110 , L111 , L112 , L115 , L175 , AFF_1:2 , AFF_1:18;
end;
L180: R8 <> R7
proof
assume L181: R8 = R7;
L182: R7 , R2 // R7 , R3 by L181 , L170 , AFF_1:4;
L183: LIN R7 , R2 , R3 by L182 , AFF_1:def 1;
L184: LIN R2 , R3 , R7 by L183 , AFF_1:6;
L185: R7 in R15 by L184 , L102 , L103 , L108 , L171 , AFF_1:25;
thus L186: contradiction by L185 , L96 , L98 , L107 , L108 , L110 , L112 , L128 , AFF_1:18;
end;
L187: (D6 is being_line & R7 in D6) by L180 , AFF_1:24;
L188: R4 , R8 // R5 , R7 by L151 , L153 , L154 , L167 , AFF_1:39;
L189: R8 in D6 by L180 , AFF_1:24;
L190: R2 <> R8
proof
assume L191: R2 = R8;
L192: R2 , R4 // R5 , R7 by L191 , L151 , L153 , L154 , L167 , AFF_1:39;
L193: R3 , R5 // R5 , R7 by L192 , L113 , L135 , AFF_1:5;
L194: R5 , R3 // R5 , R7 by L193 , AFF_1:4;
L195: LIN R5 , R3 , R7 by L194 , AFF_1:def 1;
thus L196: contradiction by L195 , L136 , AFF_1:6;
end;
L197: (not LIN R2 , R4 , R8)
proof
assume L198: LIN R2 , R4 , R8;
L199: R2 , R4 // R2 , R8 by L198 , AFF_1:def 1;
L200: R2 , R4 // R3 , R7 by L199 , L170 , L190 , AFF_1:5;
L201: R3 , R5 // R3 , R7 by L200 , L113 , L135 , AFF_1:5;
thus L202: contradiction by L201 , L136 , AFF_1:def 1;
end;
L203: R10 in D6 by L197 , L95 , L96 , L97 , L99 , L100 , L102 , L103 , L104 , L105 , L108 , L109 , L111 , L113 , L170 , L188 , L180 , L187 , L189 , L9;
L204: R8 in R16 by L203 , L98 , L107 , L110 , L128 , L187 , L189 , AFF_1:18;
L205: R16 = D4 by L204 , L106 , L110 , L115 , L164 , L134 , L166 , L188 , AFF_1:18;
thus L206: contradiction by L205 , L96 , L98 , L99 , L102 , L108 , L110 , L112 , L155 , AFF_1:18;
end;
theorem
L207: (for R1 being AffinPlane holds (R1 is Moufangian implies R1 is satisfying_TDES_1))
proof
let R1 being AffinPlane;
assume L208: R1 is Moufangian;
let R19 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L209: R19 is being_line
and
L210: R10 in R19
and
L211: R6 in R19
and
L212: R7 in R19
and
L213: (not R2 in R19)
and
L214: R10 <> R6
and
L215: R2 <> R4
and
L216: LIN R10 , R2 , R3
and
L217: R2 , R4 // R3 , R5
and
L218: R4 , R6 // R5 , R7
and
L219: R2 , R6 // R3 , R7
and
L220: R2 , R4 // R19;
consider R22 being (Subset of R1) such that L221: R3 in R22 and L222: R19 // R22 by L209 , AFF_1:49;
L223: R22 is being_line by L222 , AFF_1:36;
set D7 = ( Line (R10 , R4) );
set D8 = ( Line (R10 , R2) );
L224: (R10 in D7 & R4 in D7) by AFF_1:15;
assume L225: (not LIN R10 , R4 , R5);
L226: R10 <> R4 by L225 , AFF_1:7;
L227: D7 is being_line by L226 , AFF_1:def 3;
L228: (not R4 in R19) by L213 , L220 , AFF_1:35;
L229: (not D7 // R22)
proof
assume L230: D7 // R22;
L231: D7 // R19 by L230 , L222 , AFF_1:44;
thus L232: contradiction by L231 , L210 , L228 , L224 , AFF_1:45;
end;
consider R8 being (Element of R1) such that L233: R8 in D7 and L234: R8 in R22 by L229 , L227 , L223 , AFF_1:58;
L235: (R10 in D8 & R2 in D8) by AFF_1:15;
L236: LIN R10 , R4 , R8 by L227 , L224 , L233 , AFF_1:21;
L237: R2 , R4 // R22 by L220 , L222 , AFF_1:43;
L238: R3 , R5 // R22 by L237 , L215 , L217 , AFF_1:32;
L239: R5 in R22 by L238 , L221 , L223 , AFF_1:23;
L240: LIN R5 , R8 , R5 by L239 , L223 , L234 , AFF_1:21;
L241: D8 is being_line by L210 , L213 , AFF_1:def 3;
L242: R3 in D8 by L241 , L210 , L213 , L216 , L235 , AFF_1:25;
L243: R5 <> R7
proof
L244: R3 , R7 // R6 , R2 by L219 , AFF_1:4;
assume L245: R5 = R7;
L246: R22 = R19 by L245 , L212 , L222 , L239 , AFF_1:45;
L247: R3 = R10 by L246 , L209 , L210 , L213 , L241 , L235 , L242 , L221 , AFF_1:18;
L248: R5 = R10 by L247 , L209 , L210 , L211 , L212 , L213 , L245 , L244 , AFF_1:48;
thus L249: contradiction by L248 , L225 , AFF_1:7;
end;
L250: R4 <> R6 by L211 , L213 , L220 , AFF_1:35;
L251: R3 , R8 // R19 by L221 , L222 , L234 , AFF_1:40;
L252: R2 , R4 // R3 , R8 by L251 , L209 , L220 , AFF_1:31;
L253: R4 , R6 // R8 , R7 by L252 , L208 , L209 , L210 , L211 , L212 , L213 , L214 , L215 , L216 , L219 , L220 , L236 , L12;
L254: R5 , R7 // R8 , R7 by L253 , L218 , L250 , AFF_1:5;
L255: R7 , R5 // R7 , R8 by L254 , AFF_1:4;
L256: LIN R7 , R5 , R8 by L255 , AFF_1:def 1;
L257: LIN R5 , R8 , R7 by L256 , AFF_1:6;
L258: R3 <> R5
proof
assume L259: R3 = R5;
L260:
now
assume L261: R3 = R7;
L262: R5 = R10 by L261 , L209 , L210 , L212 , L213 , L241 , L235 , L242 , L259 , AFF_1:18;
thus L263: contradiction by L262 , L225 , AFF_1:7;
end;
L264: (R2 , R6 // R4 , R6 or R3 = R7) by L218 , L219 , L259 , AFF_1:5;
L265: R6 , R2 // R6 , R4 by L264 , L260 , AFF_1:4;
L266: LIN R6 , R2 , R4 by L265 , AFF_1:def 1;
L267: LIN R2 , R6 , R4 by L266 , AFF_1:6;
L268: R2 , R6 // R2 , R4 by L267 , AFF_1:def 1;
L269: R2 , R4 // R2 , R6 by L268 , AFF_1:4;
L270: R2 , R6 // R19 by L269 , L215 , L220 , AFF_1:32;
L271: R6 , R2 // R19 by L270 , AFF_1:34;
thus L272: contradiction by L271 , L209 , L211 , L213 , AFF_1:23;
end;
L273: LIN R5 , R8 , R3 by L221 , L223 , L234 , L239 , AFF_1:21;
L274: LIN R5 , R7 , R3 by L273 , L225 , L236 , L257 , L240 , AFF_1:8;
L275: R5 , R7 // R5 , R3 by L274 , AFF_1:def 1;
L276: R5 , R7 // R3 , R5 by L275 , AFF_1:4;
L277: R4 , R6 // R3 , R5 by L276 , L218 , L243 , AFF_1:5;
L278: R2 , R4 // R4 , R6 by L277 , L217 , L258 , AFF_1:5;
L279: R4 , R6 // R19 by L278 , L215 , L220 , AFF_1:32;
L280: R6 , R4 // R19 by L279 , AFF_1:34;
thus L281: contradiction by L280 , L209 , L211 , L228 , AFF_1:23;
end;
theorem
L282: (for R1 being AffinPlane holds (R1 is satisfying_TDES_1 implies R1 is satisfying_TDES_2))
proof
let R1 being AffinPlane;
assume L283: R1 is satisfying_TDES_1;
let R19 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L284: R19 is being_line
and
L285: R10 in R19
and
L286: R6 in R19
and
L287: R7 in R19
and
L288: (not R2 in R19)
and
L289: R10 <> R6
and
L290: R2 <> R4
and
L291: LIN R10 , R2 , R3
and
L292: LIN R10 , R4 , R5
and
L293: R4 , R6 // R5 , R7
and
L294: R2 , R6 // R3 , R7
and
L295: R2 , R4 // R19;
set D9 = ( Line (R10 , R2) );
set D10 = ( Line (R10 , R4) );
L296: (D9 is being_line & R2 in D9) by L285 , L288 , AFF_1:24;
L297: R10 in D9 by L285 , L288 , AFF_1:24;
L298: R3 in D9 by L297 , L285 , L288 , L291 , L296 , AFF_1:25;
L299: R10 <> R4 by L285 , L288 , L295 , AFF_1:35;
L300: D10 is being_line by L299 , AFF_1:24;
consider R21 being (Subset of R1) such that L301: R3 in R21 and L302: R19 // R21 by L284 , AFF_1:49;
L303: R21 is being_line by L302 , AFF_1:36;
set D11 = ( Line (R5 , R7) );
L304: (not R4 in R19) by L288 , L295 , AFF_1:35;
L305: R4 in D10 by L299 , AFF_1:24;
L306: R10 in D10 by L299 , AFF_1:24;
L307: R5 in D10 by L306 , L292 , L299 , L300 , L305 , AFF_1:25;
assume L308: (not R2 , R4 // R3 , R5);
L309: R3 <> R5 by L308 , AFF_1:3;
L310: (not R5 in R19)
proof
L311: R3 , R7 // R2 , R6 by L294 , AFF_1:4;
L312: R5 , R7 // R6 , R4 by L293 , AFF_1:4;
assume L313: R5 in R19;
L314: R5 = R10 by L313 , L284 , L285 , L304 , L300 , L306 , L305 , L307 , AFF_1:18;
L315: R7 in D9 by L314 , L284 , L285 , L286 , L287 , L304 , L297 , L312 , AFF_1:48;
L316: (R3 = R7 or R6 in D9) by L315 , L296 , L298 , L311 , AFF_1:48;
thus L317: contradiction by L316 , L284 , L285 , L286 , L287 , L288 , L289 , L309 , L304 , L297 , L296 , L313 , L312 , AFF_1:18 , AFF_1:48;
end;
L318: D11 is being_line by L310 , L287 , AFF_1:24;
L319: R5 in D11 by L287 , L310 , AFF_1:24;
L320: R7 in D11 by L287 , L310 , AFF_1:24;
L321: (not R21 // D11)
proof
assume L322: R21 // D11;
L323: R19 // D11 by L322 , L302 , AFF_1:44;
thus L324: contradiction by L323 , L287 , L310 , L319 , L320 , AFF_1:45;
end;
consider R8 being (Element of R1) such that L325: R8 in R21 and L326: R8 in D11 by L321 , L318 , L303 , AFF_1:58;
L327: R3 , R8 // R19 by L301 , L302 , L325 , AFF_1:40;
L328: R2 , R4 // R3 , R8 by L327 , L284 , L295 , AFF_1:31;
L329: LIN R7 , R5 , R8 by L318 , L319 , L320 , L326 , AFF_1:21;
L330: R7 , R5 // R7 , R8 by L329 , AFF_1:def 1;
L331: R5 , R7 // R8 , R7 by L330 , AFF_1:4;
L332: R4 , R6 // R8 , R7 by L331 , L287 , L293 , L310 , AFF_1:5;
L333: LIN R10 , R4 , R8 by L332 , L283 , L284 , L285 , L286 , L287 , L288 , L289 , L290 , L291 , L294 , L295 , L328 , L14;
L334: R8 in D10 by L333 , L299 , L300 , L306 , L305 , AFF_1:25;
L335: D10 = D11 by L334 , L308 , L300 , L307 , L318 , L319 , L326 , L328 , AFF_1:18;
L336: LIN R7 , R5 , R4 by L335 , L300 , L305 , L319 , L320 , AFF_1:21;
L337: R7 , R5 // R7 , R4 by L336 , AFF_1:def 1;
L338: R5 , R7 // R4 , R7 by L337 , AFF_1:4;
L339: R4 , R6 // R4 , R7 by L338 , L287 , L293 , L310 , AFF_1:5;
L340: LIN R4 , R6 , R7 by L339 , AFF_1:def 1;
L341: LIN R6 , R7 , R4 by L340 , AFF_1:6;
L342: R2 , R6 // R3 , R6 by L341 , L284 , L286 , L287 , L294 , L304 , AFF_1:25;
L343: R6 , R2 // R6 , R3 by L342 , AFF_1:4;
L344: LIN R6 , R2 , R3 by L343 , AFF_1:def 1;
L345: LIN R2 , R3 , R6 by L344 , AFF_1:6;
L346: (R2 = R3 or R6 in D9) by L345 , L296 , L298 , AFF_1:25;
L347: R4 , R6 // R5 , R6 by L284 , L286 , L287 , L293 , L304 , L341 , AFF_1:25;
L348: R6 , R4 // R6 , R5 by L347 , AFF_1:4;
L349: LIN R6 , R4 , R5 by L348 , AFF_1:def 1;
L350: LIN R4 , R5 , R6 by L349 , AFF_1:6;
L351: (R4 = R5 or R6 in D10) by L350 , L300 , L305 , L307 , AFF_1:25;
thus L352: contradiction by L351 , L284 , L285 , L286 , L288 , L289 , L308 , L304 , L300 , L297 , L296 , L306 , L305 , L346 , AFF_1:2 , AFF_1:18;
end;
theorem
L353: (for R1 being AffinPlane holds (R1 is satisfying_TDES_2 implies R1 is satisfying_TDES_3))
proof
let R1 being AffinPlane;
assume L354: R1 is satisfying_TDES_2;
let R19 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L355: R19 is being_line
and
L356: R10 in R19
and
L357: R6 in R19
and
L358: (not R2 in R19)
and
L359: R10 <> R6
and
L360: R2 <> R4
and
L361: LIN R10 , R2 , R3
and
L362: LIN R10 , R4 , R5
and
L363: R2 , R4 // R3 , R5
and
L364: R2 , R6 // R3 , R7
and
L365: R4 , R6 // R5 , R7
and
L366: R2 , R4 // R19;
set D12 = ( Line (R10 , R2) );
set D13 = ( Line (R10 , R4) );
set D14 = ( Line (R4 , R6) );
L367: R10 in D12 by L356 , L358 , AFF_1:24;
L368: (not LIN R2 , R4 , R6)
proof
assume L369: LIN R2 , R4 , R6;
L370: R2 , R4 // R2 , R6 by L369 , AFF_1:def 1;
L371: R2 , R6 // R19 by L370 , L360 , L366 , AFF_1:32;
L372: R6 , R2 // R19 by L371 , AFF_1:34;
thus L373: contradiction by L372 , L355 , L357 , L358 , AFF_1:23;
end;
L374: R10 <> R4 by L356 , L358 , L366 , AFF_1:35;
L375: R4 in D13 by L374 , AFF_1:24;
L376: R3 , R5 // R4 , R2 by L363 , AFF_1:4;
L377: R4 <> R6 by L357 , L358 , L366 , AFF_1:35;
L378: (R4 in D14 & R6 in D14) by L377 , AFF_1:24;
L379: R2 in D12 by L356 , L358 , AFF_1:24;
L380: D12 is being_line by L356 , L358 , AFF_1:24;
L381: D12 <> D13
proof
assume L382: D12 = D13;
L383: R2 , R4 // D12 by L382 , L380 , L379 , L375 , AFF_1:40 , AFF_1:41;
thus L384: contradiction by L383 , L356 , L358 , L360 , L366 , L367 , L379 , AFF_1:45 , AFF_1:53;
end;
assume L385: (not R7 in R19);
L386: D13 is being_line by L374 , AFF_1:24;
L387: R10 in D13 by L374 , AFF_1:24;
L388: R5 in D13 by L387 , L362 , L374 , L386 , L375 , AFF_1:25;
L389: R3 in D12 by L356 , L358 , L361 , L380 , L367 , L379 , AFF_1:25;
L390: R3 <> R5
proof
assume L391: R3 = R5;
L392: (R2 , R6 // R4 , R6 or R3 = R7) by L391 , L364 , L365 , AFF_1:5;
L393: (R6 , R2 // R6 , R4 or R3 = R7) by L392 , AFF_1:4;
L394: ( LIN R6 , R2 , R4 or R3 = R7) by L393 , AFF_1:def 1;
thus L395: contradiction by L394 , L356 , L385 , L368 , L380 , L386 , L367 , L387 , L389 , L388 , L381 , L391 , AFF_1:6 , AFF_1:18;
end;
L396: R3 <> R7
proof
assume L397: R3 = R7;
L398: R4 , R6 // R3 , R5 by L397 , L365 , AFF_1:4;
L399: R2 , R4 // R4 , R6 by L398 , L363 , L390 , AFF_1:5;
L400: R4 , R2 // R4 , R6 by L399 , AFF_1:4;
L401: LIN R4 , R2 , R6 by L400 , AFF_1:def 1;
thus L402: contradiction by L401 , L368 , AFF_1:6;
end;
L403: (not R3 , R7 // R19)
proof
assume L404: R3 , R7 // R19;
L405: R3 , R7 // R2 , R6 by L364 , AFF_1:4;
L406: R2 , R6 // R19 by L405 , L396 , L404 , AFF_1:32;
L407: R6 , R2 // R19 by L406 , AFF_1:34;
thus L408: contradiction by L407 , L355 , L357 , L358 , AFF_1:23;
end;
consider R8 being (Element of R1) such that L409: R8 in R19 and L410: LIN R3 , R7 , R8 by L403 , L355 , AFF_1:59;
L411: R3 , R7 // R3 , R8 by L410 , AFF_1:def 1;
L412: R2 , R6 // R3 , R8 by L411 , L364 , L396 , AFF_1:5;
L413: D14 is being_line by L377 , AFF_1:24;
consider R23 being (Subset of R1) such that L414: R8 in R23 and L415: D14 // R23 by L413 , AFF_1:49;
L416: (not R4 in R19) by L358 , L366 , AFF_1:35;
L417: (not R23 // D13)
proof
assume L418: R23 // D13;
L419: D14 // D13 by L418 , L415 , AFF_1:44;
L420: R6 in D13 by L419 , L375 , L378 , AFF_1:45;
thus L421: contradiction by L420 , L355 , L356 , L357 , L359 , L416 , L386 , L387 , L375 , AFF_1:18;
end;
L422: R23 is being_line by L415 , AFF_1:36;
consider R9 being (Element of R1) such that L423: R9 in R23 and L424: R9 in D13 by L422 , L386 , L417 , AFF_1:58;
L425: R4 , R6 // R9 , R8 by L378 , L414 , L415 , L423 , AFF_1:39;
L426:
now
assume L427: R9 = R5;
L428: R5 , R7 // R5 , R8 by L427 , L365 , L377 , L425 , AFF_1:5;
L429: LIN R5 , R7 , R8 by L428 , AFF_1:def 1;
L430: LIN R7 , R8 , R5 by L429 , AFF_1:6;
L431: ( LIN R7 , R8 , R3 & LIN R7 , R8 , R7) by L410 , AFF_1:6 , AFF_1:7;
L432: LIN R3 , R5 , R7 by L431 , L385 , L409 , L430 , AFF_1:8;
L433: R3 , R5 // R3 , R7 by L432 , AFF_1:def 1;
L434: R3 , R5 // R2 , R6 by L433 , L364 , L396 , AFF_1:5;
L435: R2 , R4 // R2 , R6 by L434 , L363 , L390 , AFF_1:5;
thus L436: contradiction by L435 , L368 , AFF_1:def 1;
end;
L437: LIN R10 , R4 , R9 by L386 , L387 , L375 , L424 , AFF_1:21;
L438: R2 , R4 // R3 , R9 by L437 , L354 , L355 , L356 , L357 , L358 , L359 , L360 , L361 , L366 , L409 , L425 , L412 , L16;
L439: R3 , R5 // R3 , R9 by L438 , L360 , L363 , AFF_1:5;
L440: LIN R3 , R5 , R9 by L439 , AFF_1:def 1;
L441: LIN R5 , R9 , R3 by L440 , AFF_1:6;
L442: R3 in D13 by L441 , L386 , L388 , L424 , L426 , AFF_1:25;
L443: R2 in D13 by L442 , L386 , L375 , L388 , L390 , L376 , AFF_1:48;
thus L444: contradiction by L443 , L356 , L358 , L386 , L387 , L381 , AFF_1:24;
end;
theorem
L445: (for R1 being AffinPlane holds (R1 is satisfying_TDES_3 implies R1 is Moufangian))
proof
let R1 being AffinPlane;
assume L446: R1 is satisfying_TDES_3;
let R19 being (Subset of R1);
let R10 being (Element of R1);
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
let R3 being (Element of R1);
let R5 being (Element of R1);
let R7 being (Element of R1);
assume that
L447: R19 is being_line
and
L448: R10 in R19
and
L449: R6 in R19
and
L450: R7 in R19
and
L451: (not R2 in R19)
and
L452: R10 <> R6
and
L453: R2 <> R4
and
L454: LIN R10 , R2 , R3
and
L455: LIN R10 , R4 , R5
and
L456: R2 , R4 // R3 , R5
and
L457: R2 , R6 // R3 , R7
and
L458: R2 , R4 // R19;
set D15 = ( Line (R10 , R2) );
set D16 = ( Line (R10 , R4) );
set D17 = ( Line (R4 , R6) );
set D18 = ( Line (R3 , R7) );
L459: R10 in D15 by L448 , L451 , AFF_1:24;
assume L460: (not R4 , R6 // R5 , R7);
L461: R4 <> R6 by L460 , AFF_1:3;
L462: R4 in D17 by L461 , AFF_1:24;
L463: R3 , R5 // R4 , R2 by L456 , AFF_1:4;
L464: R6 in D17 by L461 , AFF_1:24;
L465: R2 in D15 by L448 , L451 , AFF_1:24;
L466: D15 is being_line by L448 , L451 , AFF_1:24;
L467: R3 in D15 by L466 , L448 , L451 , L454 , L459 , L465 , AFF_1:25;
L468: R10 <> R4 by L448 , L451 , L458 , AFF_1:35;
L469: D16 is being_line by L468 , AFF_1:24;
L470: R4 in D16 by L468 , AFF_1:24;
L471: D15 <> D16
proof
assume L472: D15 = D16;
L473: R2 , R4 // D15 by L472 , L466 , L465 , L470 , AFF_1:40 , AFF_1:41;
thus L474: contradiction by L473 , L448 , L451 , L453 , L458 , L459 , L465 , AFF_1:45 , AFF_1:53;
end;
L475: R10 in D16 by L468 , AFF_1:24;
L476: R5 in D16 by L475 , L455 , L468 , L469 , L470 , AFF_1:25;
L477: R3 <> R5
proof
L478: R3 , R7 // R6 , R2 by L457 , AFF_1:4;
assume L479: R3 = R5;
L480: R3 in R19 by L479 , L448 , L466 , L469 , L459 , L475 , L467 , L476 , L471 , AFF_1:18;
L481: R3 = R7 by L480 , L447 , L449 , L450 , L451 , L478 , AFF_1:48;
thus L482: contradiction by L481 , L460 , L479 , AFF_1:3;
end;
L483: R3 <> R7
proof
assume L484: R3 = R7;
L485: R3 in D16 by L484 , L447 , L448 , L450 , L451 , L466 , L459 , L465 , L475 , L467 , AFF_1:18;
L486: R3 , R5 // R4 , R2 by L456 , AFF_1:4;
L487: R2 in D16 by L486 , L469 , L470 , L476 , L477 , L485 , AFF_1:48;