let r1, r2, r19, r29 be Real; :: thesis: ( r1 <> r2 & r19 <> r29 implies [.r1,r2,r19,r29.] is special_polygonal )
assume that
A1: r1 <> r2 and
A2: r19 <> r29 ; :: thesis: [.r1,r2,r19,r29.] is special_polygonal
set p1 = |[r1,r19]|;
set p2 = |[r1,r29]|;
set p3 = |[r2,r29]|;
set p4 = |[r2,r19]|;
A3: |[r2,r29]| `1 = r2 by EUCLID:52;
take |[r1,r19]| ; :: according to SPPOL_2:def 2 :: thesis: ex p2 being Point of (TOP-REAL 2) st |[r1,r19]|,p2 split [.r1,r2,r19,r29.]
take |[r2,r29]| ; :: thesis: |[r1,r19]|,|[r2,r29]| split [.r1,r2,r19,r29.]
thus |[r1,r19]| <> |[r2,r29]| by A1, FINSEQ_1:77; :: according to SPPOL_2:def 1 :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
A4: |[r2,r19]| `1 = r2 by EUCLID:52;
A5: |[r2,r29]| `2 = r29 by EUCLID:52;
A6: |[r2,r19]| `2 = r19 by EUCLID:52;
set f1 = <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*>;
set f2 = <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*>;
A7: |[r1,r19]| `1 = r1 by EUCLID:52;
A8: len <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*> = 3 by FINSEQ_1:45;
A9: len <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*> = 3 by FINSEQ_1:45;
A10: |[r1,r19]| `2 = r19 by EUCLID:52;
then reconsider f1 = <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*>, f2 = <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*> as S-Sequence_in_R2 by A1, A2, A7, A3, A5, TOPREAL3:34, TOPREAL3:35;
take f1 ; :: thesis: ex f2 being S-Sequence_in_R2 st
( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
take f2 ; :: thesis: ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
thus ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) ) by A9, A8, FINSEQ_4:18; :: thesis: ( (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) )
A11: L~ f2 = (LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|)) by TOPREAL3:16;
L~ f1 = (LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|)) by TOPREAL3:16;
hence (L~ f1) /\ (L~ f2) = (((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) /\ (LSeg (|[r2,r29]|,|[r2,r19]|))) \/ (((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) /\ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A11, XBOOLE_1:23
.= (((LSeg (|[r1,r29]|,|[r1,r19]|)) \/ (LSeg (|[r2,r29]|,|[r1,r29]|))) /\ (LSeg (|[r2,r19]|,|[r2,r29]|))) \/ {|[r1,r19]|} by A2, A7, A10, A5, A6, TOPREAL3:27
.= {|[r2,r29]|} \/ {|[r1,r19]|} by A1, A7, A3, A5, A4, TOPREAL3:28
.= {|[r1,r19]|,|[r2,r29]|} by ENUMSET1:1 ;
:: thesis: [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2)
thus [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) by A11, TOPREAL3:16; :: thesis: verum