/
aff_1.miz
1443 lines (1431 loc) · 57 KB
/
aff_1.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
:: Parallelity and Lines in Affine Spaces
:: by Henryk Oryszczyszyn and Krzysztof Pra\.zmowski
::
:: Received May 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 DIRAF, SUBSET_1, ANALOAF, INCSP_1, STRUCT_0, TARSKI, AFF_1;
notations TARSKI, STRUCT_0, ANALOAF, DIRAF;
constructors DIRAF;
registrations STRUCT_0;
requirements SUBSET, BOOLE;
theorems DIRAF, TARSKI, XBOOLE_0;
schemes SUBSET_1;
begin
definition
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
pred LIN R2 , R4 , R6
means
:L1: R2 , R4 // R2 , R6
;end;
theorem
L3: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (ex R4 being (Element of R1) st R2 <> R4)))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
consider R13 being (Element of R1), R14 being (Element of R1) such that L4: R13 <> R14 by DIRAF:40;
L5: (R2 = R13 implies R2 <> R14) by L4;
thus L6: thesis by L5;
end;
theorem
L7: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (R13 , R14 // R14 , R13 & R13 , R14 // R13 , R14))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
thus L8: R13 , R14 // R14 , R13 by DIRAF:40;
thus L9: thesis by DIRAF:40;
end;
L10: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds (R13 , R14 // R15 , R16 implies R15 , R16 // R13 , R14))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
assume L11: R13 , R14 // R15 , R16;
L12:
now
assume L13: R13 <> R14;
L14: R13 , R14 // R13 , R14 by L7;
thus L15: thesis by L14 , L11 , L13 , DIRAF:40;
end;
thus L16: thesis by L12 , DIRAF:40;
end;
theorem
L17: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (R13 , R14 // R15 , R15 & R15 , R15 // R13 , R14)))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
thus L18: R13 , R14 // R15 , R15 by DIRAF:40;
thus L19: thesis by L18 , L10;
end;
L20: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds (R13 , R14 // R15 , R16 implies R14 , R13 // R15 , R16))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
assume L21: R13 , R14 // R15 , R16;
L22: R13 , R14 // R14 , R13 by L7;
L23: (R14 , R13 // R15 , R16 or R13 = R14) by L22 , L21 , DIRAF:40;
thus L24: thesis by L23 , L17;
end;
L25: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds (R13 , R14 // R15 , R16 implies R13 , R14 // R16 , R15))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
assume L26: R13 , R14 // R15 , R16;
L27: R15 , R16 // R13 , R14 by L26 , L10;
L28: R16 , R15 // R13 , R14 by L27 , L20;
thus L29: thesis by L28 , L10;
end;
theorem
L30: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds (R13 , R14 // R15 , R16 implies (R13 , R14 // R16 , R15 & R14 , R13 // R15 , R16 & R14 , R13 // R16 , R15 & R15 , R16 // R13 , R14 & R15 , R16 // R14 , R13 & R16 , R15 // R13 , R14 & R16 , R15 // R14 , R13)))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
assume L31: R13 , R14 // R15 , R16;
thus L32: (R13 , R14 // R16 , R15 & R14 , R13 // R15 , R16) by L31 , L20 , L25;
thus L33: R14 , R13 // R16 , R15 by L32 , L20;
thus L34: R15 , R16 // R13 , R14 by L31 , L10;
thus L35: (R15 , R16 // R14 , R13 & R16 , R15 // R13 , R14) by L34 , L20 , L25;
thus L36: thesis by L35 , L25;
end;
theorem
L37: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds ((R2 <> R4 & ((R2 , R4 // R13 , R14 & R2 , R4 // R15 , R16) or (R2 , R4 // R13 , R14 & R15 , R16 // R2 , R4) or (R13 , R14 // R2 , R4 & R15 , R16 // R2 , R4) or (R13 , R14 // R2 , R4 & R2 , R4 // R15 , R16))) implies R13 , R14 // R15 , R16))))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
assume that
L38: R2 <> R4
and
L39: ((R2 , R4 // R13 , R14 & R2 , R4 // R15 , R16) or (R2 , R4 // R13 , R14 & R15 , R16 // R2 , R4) or (R13 , R14 // R2 , R4 & R15 , R16 // R2 , R4) or (R13 , R14 // R2 , R4 & R2 , R4 // R15 , R16));
L40: R2 , R4 // R15 , R16 by L39 , L30;
L41: R2 , R4 // R13 , R14 by L39 , L30;
thus L42: thesis by L41 , L38 , L40 , DIRAF:40;
end;
L43: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds ( LIN R13 , R14 , R15 implies ( LIN R13 , R15 , R14 & LIN R14 , R13 , R15))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
assume L44: LIN R13 , R14 , R15;
L45: R13 , R14 // R13 , R15 by L44 , L1;
L46: R14 , R13 // R14 , R15 by L45 , DIRAF:40;
L47: R13 , R15 // R13 , R14 by L45 , L30;
thus L48: thesis by L47 , L46 , L1;
end;
theorem
L49: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds ( LIN R13 , R14 , R15 implies ( LIN R13 , R15 , R14 & LIN R14 , R13 , R15 & LIN R14 , R15 , R13 & LIN R15 , R13 , R14 & LIN R15 , R14 , R13))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
assume L50: LIN R13 , R14 , R15;
thus L51: ( LIN R13 , R15 , R14 & LIN R14 , R13 , R15) by L50 , L43;
thus L52: ( LIN R14 , R15 , R13 & LIN R15 , R13 , R14) by L51 , L43;
thus L53: thesis by L52 , L43;
end;
theorem
L54: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds ( LIN R13 , R13 , R14 & LIN R13 , R14 , R14 & LIN R13 , R14 , R13))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
L55: R13 , R14 // R13 , R14 by L7;
L56: R13 , R14 // R13 , R13 by L17;
L57: R13 , R13 // R13 , R14 by L17;
thus L58: thesis by L57 , L55 , L56 , L1;
end;
theorem
L59: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds (for R17 being (Element of R1) holds ((R13 <> R14 & LIN R13 , R14 , R15 & LIN R13 , R14 , R16 & LIN R13 , R14 , R17) implies LIN R15 , R16 , R17)))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
let R17 being (Element of R1);
assume that
L60: R13 <> R14
and
L61: LIN R13 , R14 , R15
and
L62: LIN R13 , R14 , R16
and
L63: LIN R13 , R14 , R17;
L64:
now
L65: R13 , R14 // R13 , R15 by L61 , L1;
L66: R13 , R14 // R13 , R17 by L63 , L1;
L67: R13 , R15 // R13 , R17 by L66 , L60 , L65 , L37;
L68: R15 , R13 // R15 , R17 by L67 , DIRAF:40;
L69: R13 , R14 // R13 , R16 by L62 , L1;
L70: R13 , R15 // R13 , R16 by L69 , L60 , L65 , L37;
L71: R15 , R13 // R15 , R16 by L70 , DIRAF:40;
assume L72: R13 <> R15;
L73: R15 , R16 // R15 , R17 by L72 , L71 , L68 , L37;
thus L74: thesis by L73 , L1;
end;
L75:
now
assume L76: R13 = R15;
L77: R15 , R14 // R15 , R17 by L76 , L63 , L1;
L78: R15 , R14 // R15 , R16 by L62 , L76 , L1;
L79: R15 , R16 // R15 , R17 by L78 , L60 , L76 , L77 , L37;
thus L80: thesis by L79 , L1;
end;
thus L81: thesis by L75 , L64;
end;
theorem
L82: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds ((R13 <> R14 & LIN R13 , R14 , R15 & R13 , R14 // R15 , R16) implies LIN R13 , R14 , R16))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
assume that
L83: R13 <> R14
and
L84: LIN R13 , R14 , R15
and
L85: R13 , R14 // R15 , R16;
L86:
now
L87: R13 , R14 // R13 , R15 by L84 , L1;
L88: R13 , R15 // R15 , R16 by L87 , L83 , L85 , L37;
L89: R15 , R13 // R15 , R16 by L88 , L30;
L90: LIN R15 , R13 , R16 by L89 , L1;
L91: LIN R13 , R15 , R16 by L90 , L49;
assume L92: R15 <> R13;
L93: LIN R13 , R15 , R13 by L54;
L94: LIN R13 , R15 , R14 by L84 , L49;
thus L95: thesis by L94 , L92 , L91 , L93 , L59;
end;
thus L96: thesis by L86 , L85 , L1;
end;
theorem
L97: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R16 being (Element of R1) holds (( LIN R13 , R14 , R15 & LIN R13 , R14 , R16) implies R13 , R14 // R15 , R16))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R16 being (Element of R1);
assume that
L98: LIN R13 , R14 , R15
and
L99: LIN R13 , R14 , R16;
L100:
now
L101: R13 , R14 // R13 , R16 by L99 , L1;
L102: R13 , R14 // R13 , R15 by L98 , L1;
assume L103: R13 <> R14;
L104: R13 , R15 // R13 , R16 by L103 , L102 , L101 , L37;
L105: R15 , R13 // R15 , R16 by L104 , DIRAF:40;
L106: R13 , R15 // R15 , R16 by L105 , L30;
thus L107: thesis by L106 , L102 , L101 , L37;
end;
thus L108: thesis by L100 , L17;
end;
theorem
L109: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (for R15 being (Element of R1) holds (for R17 being (Element of R1) holds (for R18 being (Element of R1) holds ((R17 <> R15 & LIN R13 , R14 , R17 & LIN R13 , R14 , R15 & LIN R17 , R15 , R18) implies LIN R13 , R14 , R18)))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
let R15 being (Element of R1);
let R17 being (Element of R1);
let R18 being (Element of R1);
assume that
L110: R17 <> R15
and
L111: LIN R13 , R14 , R17
and
L112: LIN R13 , R14 , R15
and
L113: LIN R17 , R15 , R18;
L114:
now
assume L115: R13 <> R14;
L116: LIN R13 , R14 , R13 by L54;
L117: LIN R15 , R17 , R13 by L116 , L111 , L112 , L115 , L59;
L118: LIN R13 , R14 , R14 by L54;
L119: LIN R15 , R17 , R14 by L118 , L111 , L112 , L115 , L59;
L120: LIN R15 , R17 , R18 by L113 , L49;
thus L121: thesis by L120 , L110 , L119 , L117 , L59;
end;
thus L122: thesis by L114 , L54;
end;
theorem
L123: (for R1 being AffinSpace holds (ex R13 being (Element of R1) st (ex R14 being (Element of R1) st (ex R15 being (Element of R1) st (not LIN R13 , R14 , R15)))))
proof
let R1 being AffinSpace;
consider R13 being (Element of R1), R14 being (Element of R1), R15 being (Element of R1) such that L124: (not R13 , R14 // R13 , R15) by DIRAF:40;
L125: (not LIN R13 , R14 , R15) by L124 , L1;
thus L126: thesis by L125;
end;
theorem
L127: (for R1 being AffinSpace holds (for R13 being (Element of R1) holds (for R14 being (Element of R1) holds (R13 <> R14 implies (ex R15 being (Element of R1) st (not LIN R13 , R14 , R15))))))
proof
let R1 being AffinSpace;
let R13 being (Element of R1);
let R14 being (Element of R1);
assume L128: R13 <> R14;
consider R2 being (Element of R1), R4 being (Element of R1), R6 being (Element of R1) such that L129: (not LIN R2 , R4 , R6) by L123;
assume L130: (not thesis);
L131: LIN R13 , R14 , R4 by L130;
L132: LIN R13 , R14 , R6 by L130;
L133: LIN R13 , R14 , R2 by L130;
thus L134: contradiction by L133 , L128 , L129 , L131 , L132 , L59;
end;
theorem
L135: (for R1 being AffinSpace 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 (((not LIN R8 , R2 , R4) & LIN R8 , R4 , R5 & R2 , R4 // R2 , R5) implies R4 = R5))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R5 being (Element of R1);
let R8 being (Element of R1);
assume that
L136: (not LIN R8 , R2 , R4)
and
L137: LIN R8 , R4 , R5
and
L138: R2 , R4 // R2 , R5;
L139: LIN R2 , R4 , R5 by L138 , L1;
L140: LIN R4 , R5 , R2 by L139 , L49;
L141: LIN R4 , R5 , R4 by L54;
assume L142: R4 <> R5;
L143: LIN R4 , R5 , R8 by L137 , L49;
thus L144: contradiction by L143 , L136 , L142 , L140 , L141 , L59;
end;
definition
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
func Line (R2 , R4) -> (Subset of R1) means
:L145: (for R13 being (Element of R1) holds (R13 in it iff LIN R2 , R4 , R13));
existence
proof
defpred S1[ set ] means (for R14 being (Element of R1) holds (R14 = $1 implies LIN R2 , R4 , R14));
consider C1 being (Subset of R1) such that L146: (for B1 being set holds (B1 in C1 iff (B1 in (the carrier of R1) & S1[ B1 ]))) from SUBSET_1:sch 1;
take C1;
let R13 being (Element of R1);
thus L147: (R13 in C1 implies LIN R2 , R4 , R13) by L146;
assume L148: LIN R2 , R4 , R13;
L149: (for R14 being (Element of R1) holds (R14 = R13 implies LIN R2 , R4 , R14)) by L148;
thus L150: thesis by L149 , L146;
end;
uniqueness
proof
let C2 , C3 being (Subset of R1);
assume that
L151: (for R13 being (Element of R1) holds (R13 in C2 iff LIN R2 , R4 , R13))
and
L152: (for R13 being (Element of R1) holds (R13 in C3 iff LIN R2 , R4 , R13));
L153: (for B2 being set holds (B2 in C2 iff B2 in C3))
proof
let C4 being set;
thus L154: (C4 in C2 implies C4 in C3)
proof
assume L155: C4 in C2;
reconsider D1 = C4 as (Element of R1) by L155;
L156: LIN R2 , R4 , D1 by L151 , L155;
thus L157: thesis by L156 , L152;
end;
assume L158: C4 in C3;
reconsider D2 = C4 as (Element of R1) by L158;
L159: LIN R2 , R4 , D2 by L152 , L158;
thus L160: thesis by L159 , L151;
end;
thus L161: thesis by L153 , TARSKI:1;
end;
end;
L163: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds ( Line (R2 , R4) ) c= ( Line (R4 , R2) ))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
L164:
now
let C5 being set;
assume L165: C5 in ( Line (R2 , R4) );
reconsider D3 = C5 as (Element of R1) by L165;
L166: LIN R2 , R4 , D3 by L165 , L145;
L167: LIN R4 , R2 , D3 by L166 , L49;
thus L168: C5 in ( Line (R4 , R2) ) by L167 , L145;
end;
thus L169: thesis by L164 , TARSKI:def 3;
end;
definition
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
redefine func Line (R2 , R4);
commutativity
proof
let R2 being (Element of R1);
let R4 being (Element of R1);
L170: ( Line (R4 , R2) ) c= ( Line (R2 , R4) ) by L163;
L171: ( Line (R2 , R4) ) c= ( Line (R4 , R2) ) by L163;
thus L172: thesis by L171 , L170 , XBOOLE_0:def 10;
end;
end;
theorem
L174: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (R2 in ( Line (R2 , R4) ) & R4 in ( Line (R2 , R4) )))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
L175: LIN R2 , R4 , R4 by L54;
L176: LIN R2 , R4 , R2 by L54;
thus L177: thesis by L176 , L175 , L145;
end;
theorem
L178: (for R1 being AffinSpace 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 ((R6 in ( Line (R2 , R4) ) & R7 in ( Line (R2 , R4) ) & R6 <> R7) implies ( Line (R6 , R7) ) c= ( Line (R2 , R4) )))))))
proof
let R1 being AffinSpace;
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 that
L179: R6 in ( Line (R2 , R4) )
and
L180: R7 in ( Line (R2 , R4) )
and
L181: R6 <> R7;
L182: LIN R2 , R4 , R7 by L180 , L145;
L183: LIN R2 , R4 , R6 by L179 , L145;
L184:
now
let C6 being set;
assume L185: C6 in ( Line (R6 , R7) );
reconsider D4 = C6 as (Element of R1) by L185;
L186: LIN R6 , R7 , D4 by L185 , L145;
L187: LIN R2 , R4 , D4 by L186 , L181 , L183 , L182 , L109;
thus L188: C6 in ( Line (R2 , R4) ) by L187 , L145;
end;
thus L189: thesis by L184 , TARSKI:def 3;
end;
theorem
L190: (for R1 being AffinSpace 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 ((R6 in ( Line (R2 , R4) ) & R7 in ( Line (R2 , R4) ) & R2 <> R4) implies ( Line (R2 , R4) ) c= ( Line (R6 , R7) )))))))
proof
let R1 being AffinSpace;
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 that
L191: R6 in ( Line (R2 , R4) )
and
L192: R7 in ( Line (R2 , R4) )
and
L193: R2 <> R4;
L194: LIN R2 , R4 , R7 by L192 , L145;
L195: LIN R2 , R4 , R6 by L191 , L145;
L196:
now
let C7 being set;
assume L197: C7 in ( Line (R2 , R4) );
reconsider D5 = C7 as (Element of R1) by L197;
L198: LIN R2 , R4 , D5 by L197 , L145;
L199: LIN R6 , R7 , D5 by L198 , L193 , L195 , L194 , L59;
thus L200: C7 in ( Line (R6 , R7) ) by L199 , L145;
end;
thus L201: thesis by L196 , TARSKI:def 3;
end;
definition
let R1 being AffinSpace;
let R19 being (Subset of R1);
attr R19 is being_line
means
:L202: (ex R2 being (Element of R1) st (ex R4 being (Element of R1) st (R2 <> R4 & R19 = ( Line (R2 , R4) ))));
end;
registration
let R1 being AffinSpace;
cluster being_line for (Subset of R1);
existence
proof
set D6 = the (Element of R1);
consider C8 being (Element of R1) such that L204: D6 <> C8 by L3;
take ( Line (D6 , C8) );
thus L205: thesis by L204 , L202;
end;
end;
L207: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds ((R19 is being_line & R2 in R19 & R4 in R19 & R2 <> R4) implies R19 = ( Line (R2 , R4) ))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
assume that
L208: R19 is being_line
and
L209: R2 in R19
and
L210: R4 in R19
and
L211: R2 <> R4;
L212: (ex R9 being (Element of R1) st (ex R10 being (Element of R1) st (R9 <> R10 & R19 = ( Line (R9 , R10) )))) by L208 , L202;
L213: R19 c= ( Line (R2 , R4) ) by L212 , L209 , L210 , L190;
L214: ( Line (R2 , R4) ) c= R19 by L209 , L210 , L211 , L212 , L178;
thus L215: thesis by L214 , L213 , XBOOLE_0:def 10;
end;
theorem
L216: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds (for R20 being (Subset of R1) holds ((R19 is being_line & R20 is being_line & R2 in R19 & R4 in R19 & R2 in R20 & R4 in R20) implies (R2 = R4 or R19 = R20)))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
let R20 being (Subset of R1);
assume that
L217: R19 is being_line
and
L218: R20 is being_line
and
L219: R2 in R19
and
L220: R4 in R19
and
L221: R2 in R20
and
L222: R4 in R20;
assume L223: R2 <> R4;
L224: R19 = ( Line (R2 , R4) ) by L223 , L217 , L219 , L220 , L207;
thus L225: thesis by L224 , L218 , L221 , L222 , L223 , L207;
end;
theorem
L226: (for R1 being AffinSpace holds (for R19 being (Subset of R1) holds (R19 is being_line implies (ex R2 being (Element of R1) st (ex R4 being (Element of R1) st (R2 in R19 & R4 in R19 & R2 <> R4))))))
proof
let R1 being AffinSpace;
let R19 being (Subset of R1);
assume L227: R19 is being_line;
consider R2 being (Element of R1), R4 being (Element of R1) such that L228: R2 <> R4 and L229: R19 = ( Line (R2 , R4) ) by L227 , L202;
L230: R4 in R19 by L229 , L174;
L231: R2 in R19 by L229 , L174;
thus L232: thesis by L231 , L228 , L230;
end;
theorem
L233: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R19 being (Subset of R1) holds (R19 is being_line implies (ex R4 being (Element of R1) st (R2 <> R4 & R4 in R19))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R19 being (Subset of R1);
assume L234: R19 is being_line;
consider R9 being (Element of R1), R10 being (Element of R1) such that L235: R9 in R19 and L236: R10 in R19 and L237: R9 <> R10 by L234 , L226;
L238: (R2 = R9 implies (R2 <> R10 & R10 in R19)) by L236 , L237;
thus L239: thesis by L238 , L235;
end;
theorem
L240: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R6 being (Element of R1) holds ( LIN R2 , R4 , R6 iff (ex R19 being (Subset of R1) st (R19 is being_line & R2 in R19 & R4 in R19 & R6 in R19)))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R6 being (Element of R1);
L241: ( LIN R2 , R4 , R6 implies (ex R19 being (Subset of R1) st (R19 is being_line & R2 in R19 & R4 in R19 & R6 in R19)))
proof
assume L242: LIN R2 , R4 , R6;
L243:
now
set D7 = ( Line (R2 , R4) );
L244: R2 in D7 by L174;
L245: R4 in D7 by L174;
assume L246: R2 <> R4;
L247: D7 is being_line by L246 , L202;
L248: R6 in D7 by L242 , L145;
thus L249: thesis by L248 , L247 , L244 , L245;
end;
L250:
now
set D8 = ( Line (R2 , R6) );
L251: R6 in D8 by L174;
assume L252: R2 <> R6;
L253: D8 is being_line by L252 , L202;
L254: LIN R2 , R6 , R4 by L242 , L49;
L255: R4 in D8 by L254 , L145;
L256: R2 in D8 by L174;
thus L257: thesis by L256 , L253 , L255 , L251;
end;
L258:
now
consider R13 being (Element of R1) such that L259: R2 <> R13 by L3;
set D9 = ( Line (R2 , R13) );
L260: R2 in D9 by L174;
assume that
L261: R2 = R4
and
L262: R2 = R6;
L263: D9 is being_line by L259 , L202;
thus L264: thesis by L263 , L261 , L262 , L260;
end;
thus L265: thesis by L258 , L243 , L250;
end;
L266: ((ex R19 being (Subset of R1) st (R19 is being_line & R2 in R19 & R4 in R19 & R6 in R19)) implies LIN R2 , R4 , R6)
proof
given R19 being (Subset of R1) such that
L267: R19 is being_line
and
L268: R2 in R19
and
L269: R4 in R19
and
L270: R6 in R19;
consider R9 being (Element of R1), R10 being (Element of R1) such that L271: R9 <> R10 and L272: R19 = ( Line (R9 , R10) ) by L267 , L202;
L273: LIN R9 , R10 , R4 by L269 , L272 , L145;
L274: LIN R9 , R10 , R6 by L270 , L272 , L145;
L275: LIN R9 , R10 , R2 by L268 , L272 , L145;
thus L276: thesis by L275 , L271 , L273 , L274 , L59;
end;
thus L277: thesis by L266 , L241;
end;
definition
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
pred R2 , R4 // R19
means
:L278: (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R6 <> R7 & R19 = ( Line (R6 , R7) ) & R2 , R4 // R6 , R7)))
;end;
definition
let R1 being AffinSpace;
let R19 being (Subset of R1);
let R20 being (Subset of R1);
pred R19 // R20
means
:L280: (ex R2 being (Element of R1) st (ex R4 being (Element of R1) st (R19 = ( Line (R2 , R4) ) & R2 <> R4 & R2 , R4 // R20)))
;end;
theorem
L282: (for R1 being AffinSpace 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 ((R6 in ( Line (R2 , R4) ) & R2 <> R4) implies (R7 in ( Line (R2 , R4) ) iff R2 , R4 // R6 , R7)))))))
proof
let R1 being AffinSpace;
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 that
L283: R6 in ( Line (R2 , R4) )
and
L284: R2 <> R4;
L285: LIN R2 , R4 , R6 by L283 , L145;
thus L286: (R7 in ( Line (R2 , R4) ) implies R2 , R4 // R6 , R7)
proof
assume L287: R7 in ( Line (R2 , R4) );
L288: LIN R2 , R4 , R7 by L287 , L145;
thus L289: thesis by L288 , L285 , L97;
end;
assume L290: R2 , R4 // R6 , R7;
L291: LIN R2 , R4 , R7 by L290 , L284 , L285 , L82;
thus L292: thesis by L291 , L145;
end;
theorem
L293: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds ((R19 is being_line & R2 in R19) implies (R4 in R19 iff R2 , R4 // R19))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
assume that
L294: R19 is being_line
and
L295: R2 in R19;
consider R9 being (Element of R1), R10 being (Element of R1) such that L296: R9 <> R10 and L297: R19 = ( Line (R9 , R10) ) by L294 , L202;
thus L298:now
assume L299: R4 in R19;
L300: R9 , R10 // R2 , R4 by L299 , L295 , L296 , L297 , L282;
L301: R2 , R4 // R9 , R10 by L300 , L30;
thus L302: R2 , R4 // R19 by L301 , L296 , L297 , L278;
end;
assume L303: R2 , R4 // R19;
consider R9 being (Element of R1), R10 being (Element of R1) such that L304: R9 <> R10 and L305: R19 = ( Line (R9 , R10) ) and L306: R2 , R4 // R9 , R10 by L303 , L278;
L307: R9 , R10 // R2 , R4 by L306 , L30;
thus L308: R4 in R19 by L307 , L295 , L304 , L305 , L282;
end;
theorem
L309: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds ((R2 <> R4 & R19 = ( Line (R2 , R4) )) iff (R19 is being_line & R2 in R19 & R4 in R19 & R2 <> R4)))))) by L202 , L207 , L174;
theorem
L310: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R13 being (Element of R1) holds (for R19 being (Subset of R1) holds ((R19 is being_line & R2 in R19 & R4 in R19 & R2 <> R4 & LIN R2 , R4 , R13) implies R13 in R19))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R13 being (Element of R1);
let R19 being (Subset of R1);
assume that
L311: R19 is being_line
and
L312: R2 in R19
and
L313: R4 in R19
and
L314: R2 <> R4
and
L315: LIN R2 , R4 , R13;
L316: R19 = ( Line (R2 , R4) ) by L311 , L312 , L313 , L314 , L207;
thus L317: thesis by L316 , L315 , L145;
end;
theorem
L318: (for R1 being AffinSpace holds (for R19 being (Subset of R1) holds ((ex R2 being (Element of R1) st (ex R4 being (Element of R1) st R2 , R4 // R19)) implies R19 is being_line)))
proof
let R1 being AffinSpace;
let R19 being (Subset of R1);
given R2 being (Element of R1) , R4 being (Element of R1) such that
L319: R2 , R4 // R19;
L320: (ex R9 being (Element of R1) st (ex R10 being (Element of R1) st (R9 <> R10 & R19 = ( Line (R9 , R10) ) & R2 , R4 // R9 , R10))) by L319 , L278;
thus L321: thesis by L320 , L202;
end;
theorem
L322: (for R1 being AffinSpace 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 R19 being (Subset of R1) holds ((R6 in R19 & R7 in R19 & R19 is being_line & R6 <> R7) implies (R2 , R4 // R19 iff R2 , R4 // R6 , R7))))))))
proof
let R1 being AffinSpace;
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 R19 being (Subset of R1);
assume that
L323: R6 in R19
and
L324: R7 in R19
and
L325: R19 is being_line
and
L326: R6 <> R7;
thus L327: (R2 , R4 // R19 implies R2 , R4 // R6 , R7)
proof
assume L328: R2 , R4 // R19;
consider R9 being (Element of R1), R10 being (Element of R1) such that L329: R9 <> R10 and L330: R19 = ( Line (R9 , R10) ) and L331: R2 , R4 // R9 , R10 by L328 , L278;
L332: R9 , R10 // R6 , R7 by L323 , L324 , L329 , L330 , L282;
thus L333: thesis by L332 , L329 , L331 , L37;
end;
assume L334: R2 , R4 // R6 , R7;
L335: R19 = ( Line (R6 , R7) ) by L323 , L324 , L325 , L326 , L207;
thus L336: thesis by L335 , L326 , L334 , L278;
end;
theorem
L337: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds (R2 , R4 // R19 implies (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R6 <> R7 & R6 in R19 & R7 in R19 & R2 , R4 // R6 , R7))))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
assume L338: R2 , R4 // R19;
consider R6 being (Element of R1), R7 being (Element of R1) such that L339: R6 <> R7 and L340: R19 = ( Line (R6 , R7) ) and L341: R2 , R4 // R6 , R7 by L338 , L278;
L342: R7 in R19 by L340 , L174;
L343: R6 in R19 by L340 , L174;
thus L344: thesis by L343 , L339 , L341 , L342;
end;
theorem
L345: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (R2 <> R4 implies R2 , R4 // ( Line (R2 , R4) )))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
assume L346: R2 <> R4;
L347: R2 , R4 // R2 , R4 by L7;
thus L348: thesis by L347 , L346 , L278;
end;
theorem
L349: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for B3 being being_line (Subset of R1) holds (R2 , R4 // B3 iff (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R6 <> R7 & R6 in B3 & R7 in B3 & R2 , R4 // R6 , R7))))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
L350: (for R19 being (Subset of R1) holds (R2 , R4 // R19 implies (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R6 <> R7 & R6 in R19 & R7 in R19 & R2 , R4 // R6 , R7))))) by L337;
let C9 being being_line (Subset of R1);
L351: ((ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R6 <> R7 & R6 in C9 & R7 in C9 & R2 , R4 // R6 , R7))) implies R2 , R4 // C9)
proof
assume L352: (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R6 <> R7 & R6 in C9 & R7 in C9 & R2 , R4 // R6 , R7)));
consider R6 being (Element of R1), R7 being (Element of R1) such that L353: R6 <> R7 and L354: R6 in C9 and L355: R7 in C9 and L356: R2 , R4 // R6 , R7 by L352;
L357: C9 = ( Line (R6 , R7) ) by L353 , L354 , L355 , L207;
thus L358: thesis by L357 , L353 , L356 , L278;
end;
thus L359: thesis by L351 , L350;
end;
theorem
L360: (for R1 being AffinSpace 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 B4 being being_line (Subset of R1) holds ((R2 , R4 // B4 & R6 , R7 // B4) implies R2 , R4 // R6 , R7)))))))
proof
let R1 being AffinSpace;
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 C10 being being_line (Subset of R1);
assume that
L361: R2 , R4 // C10
and
L362: R6 , R7 // C10;
consider R9 being (Element of R1), R10 being (Element of R1) such that L363: R9 <> R10 and L364: C10 = ( Line (R9 , R10) ) and L365: R2 , R4 // R9 , R10 by L361 , L278;
L366: R10 in C10 by L364 , L174;
L367: R9 in C10 by L364 , L174;
L368: R6 , R7 // R9 , R10 by L367 , L362 , L363 , L366 , L322;
thus L369: thesis by L368 , L363 , L365 , L37;
end;
theorem
L370: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R9 being (Element of R1) holds (for R10 being (Element of R1) holds (for R19 being (Subset of R1) holds ((R2 , R4 // R19 & R2 , R4 // R9 , R10 & R2 <> R4) implies R9 , R10 // R19)))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R9 being (Element of R1);
let R10 being (Element of R1);
let R19 being (Subset of R1);
assume that
L371: R2 , R4 // R19
and
L372: R2 , R4 // R9 , R10
and
L373: R2 <> R4;
L374: R19 is being_line by L371 , L318;
consider R6 being (Element of R1), R7 being (Element of R1) such that L375: R6 <> R7 and L376: R6 in R19 and L377: R7 in R19 and L378: R2 , R4 // R6 , R7 by L374 , L371 , L349;
L379: R9 , R10 // R6 , R7 by L372 , L373 , L378 , L37;
thus L380: thesis by L379 , L374 , L375 , L376 , L377 , L349;
end;
theorem
L381: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for B5 being being_line (Subset of R1) holds R2 , R2 // B5)))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let C11 being being_line (Subset of R1);
consider R9 being (Element of R1), R10 being (Element of R1) such that L382: R9 <> R10 and L383: C11 = ( Line (R9 , R10) ) by L202;
L384: R2 , R2 // R9 , R10 by L17;
thus L385: thesis by L384 , L382 , L383 , L278;
end;
theorem
L386: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds (R2 , R4 // R19 implies R4 , R2 // R19)))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
assume L387: R2 , R4 // R19;
L388:
now
assume L389: R2 <> R4;
L390: R2 , R4 // R4 , R2 by L7;
thus L391: thesis by L390 , L387 , L389 , L370;
end;
thus L392: thesis by L388 , L387;
end;
theorem
L393: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds ((R2 , R4 // R19 & (not R2 in R19)) implies (not R4 in R19))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
assume that
L394: R2 , R4 // R19
and
L395: (not R2 in R19)
and
L396: R4 in R19;
L397: R4 , R2 // R19 by L394 , L386;
L398: R19 is being_line by L394 , L318;
thus L399: contradiction by L398 , L395 , L396 , L397 , L293;
end;
theorem
L400: (for R1 being AffinSpace holds (for R19 being (Subset of R1) holds (for R20 being (Subset of R1) holds (R19 // R20 implies (R19 is being_line & R20 is being_line)))))
proof
let R1 being AffinSpace;
let R19 being (Subset of R1);
let R20 being (Subset of R1);
assume L401: R19 // R20;
L402: (ex R2 being (Element of R1) st (ex R4 being (Element of R1) st (R19 = ( Line (R2 , R4) ) & R2 <> R4 & R2 , R4 // R20))) by L401 , L280;
thus L403: thesis by L402 , L202 , L318;
end;
theorem
L404: (for R1 being AffinSpace holds (for R19 being (Subset of R1) holds (for R20 being (Subset of R1) holds (R19 // R20 iff (ex R2 being (Element of R1) st (ex R4 being (Element of R1) st (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R2 <> R4 & R6 <> R7 & R2 , R4 // R6 , R7 & R19 = ( Line (R2 , R4) ) & R20 = ( Line (R6 , R7) ))))))))))
proof
let R1 being AffinSpace;
let R19 being (Subset of R1);
let R20 being (Subset of R1);
thus L405: (R19 // R20 implies (ex R2 being (Element of R1) st (ex R4 being (Element of R1) st (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R2 <> R4 & R6 <> R7 & R2 , R4 // R6 , R7 & R19 = ( Line (R2 , R4) ) & R20 = ( Line (R6 , R7) )))))))
proof
assume L406: R19 // R20;
consider R2 being (Element of R1), R4 being (Element of R1) such that L407: R19 = ( Line (R2 , R4) ) and L408: R2 <> R4 and L409: R2 , R4 // R20 by L406 , L280;
L410: (ex R6 being (Element of R1) st (ex R7 being (Element of R1) st (R6 <> R7 & R20 = ( Line (R6 , R7) ) & R2 , R4 // R6 , R7))) by L409 , L278;
thus L411: thesis by L410 , L407 , L408;
end;
given R2 being (Element of R1) , R4 being (Element of R1) , R6 being (Element of R1) , R7 being (Element of R1) such that
L412: R2 <> R4
and
L413: R6 <> R7
and
L414: R2 , R4 // R6 , R7
and
L415: R19 = ( Line (R2 , R4) )
and
L416: R20 = ( Line (R6 , R7) );
L417: R2 , R4 // R20 by L413 , L414 , L416 , L278;
thus L418: thesis by L417 , L412 , L415 , L280;
end;
theorem
L419: (for R1 being AffinSpace 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 B6 , B7 being being_line (Subset of R1) holds ((R2 in B6 & R4 in B6 & R6 in B7 & R7 in B7 & R2 <> R4 & R6 <> R7) implies (B6 // B7 iff R2 , R4 // R6 , R7))))))))
proof
let R1 being AffinSpace;
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 C12 , C13 being being_line (Subset of R1);
assume that
L420: R2 in C12
and
L421: R4 in C12
and
L422: R6 in C13
and
L423: R7 in C13
and
L424: R2 <> R4
and
L425: R6 <> R7;
thus L426: (C12 // C13 implies R2 , R4 // R6 , R7)
proof
assume L427: C12 // C13;
consider R9 being (Element of R1), R10 being (Element of R1), R11 being (Element of R1), R12 being (Element of R1) such that L428: R9 <> R10 and L429: R11 <> R12 and L430: R9 , R10 // R11 , R12 and L431: C12 = ( Line (R9 , R10) ) and L432: C13 = ( Line (R11 , R12) ) by L427 , L404;
L433: R9 , R10 // R2 , R4 by L420 , L421 , L428 , L431 , L282;
L434: R2 , R4 // R11 , R12 by L433 , L428 , L430 , L37;
L435: R11 , R12 // R6 , R7 by L422 , L423 , L429 , L432 , L282;
thus L436: thesis by L435 , L429 , L434 , L37;
end;
L437: C13 = ( Line (R6 , R7) ) by L422 , L423 , L425 , L207;
assume L438: R2 , R4 // R6 , R7;
L439: C12 = ( Line (R2 , R4) ) by L420 , L421 , L424 , L207;
thus L440: thesis by L439 , L424 , L425 , L438 , L437 , L404;
end;
theorem
L441: (for R1 being AffinSpace 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 R19 being (Subset of R1) holds (for R20 being (Subset of R1) holds ((R2 in R19 & R4 in R19 & R6 in R20 & R7 in R20 & R19 // R20) implies R2 , R4 // R6 , R7))))))))
proof
let R1 being AffinSpace;
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 R19 being (Subset of R1);
let R20 being (Subset of R1);
assume that
L442: R2 in R19
and
L443: R4 in R19
and
L444: R6 in R20
and
L445: R7 in R20
and
L446: R19 // R20;
L447:
now
L448: R20 is being_line by L446 , L400;
assume that
L449: R2 <> R4
and
L450: R6 <> R7;
L451: R19 is being_line by L446 , L400;
thus L452: thesis by L451 , L442 , L443 , L444 , L445 , L446 , L449 , L450 , L448 , L419;
end;
thus L453: thesis by L447 , L17;
end;
theorem
L454: (for R1 being AffinSpace holds (for R2 being (Element of R1) holds (for R4 being (Element of R1) holds (for R19 being (Subset of R1) holds (for R20 being (Subset of R1) holds ((R2 in R19 & R4 in R19 & R19 // R20) implies R2 , R4 // R20))))))
proof
let R1 being AffinSpace;
let R2 being (Element of R1);
let R4 being (Element of R1);
let R19 being (Subset of R1);
let R20 being (Subset of R1);
assume that
L455: R2 in R19
and
L456: R4 in R19
and
L457: R19 // R20;
L458: R20 is being_line by L457 , L400;
L459:
now
consider R9 being (Element of R1), R10 being (Element of R1) such that L460: R9 in R20 and L461: R10 in R20 and L462: R9 <> R10 by L458 , L226;
L463: R20 = ( Line (R9 , R10) ) by L458 , L460 , L461 , L462 , L207;
L464: R2 , R4 // R9 , R10 by L455 , L456 , L457 , L460 , L461 , L441;
thus L465: thesis by L464 , L462 , L463 , L278;
end;
thus L466: thesis by L459;
end;
theorem
L467: (for R1 being AffinSpace holds (for B8 being being_line (Subset of R1) holds B8 // B8))