let r1, r2, r1', r2' be real number ; :: thesis: ( r1 <> r2 & r1' <> r2' implies [.r1,r2,r1',r2'.] is special_polygonal )
assume that
A1: r1 <> r2 and
A2: r1' <> r2' ; :: thesis: [.r1,r2,r1',r2'.] is special_polygonal
set p1 = |[r1,r1']|;
set p2 = |[r1,r2']|;
set p3 = |[r2,r2']|;
set p4 = |[r2,r1']|;
take |[r1,r1']| ; :: according to SPPOL_2:def 2 :: thesis: ex p2 being Point of (TOP-REAL 2) st |[r1,r1']|,p2 split [.r1,r2,r1',r2'.]
take |[r2,r2']| ; :: thesis: |[r1,r1']|,|[r2,r2']| split [.r1,r2,r1',r2'.]
thus |[r1,r1']| <> |[r2,r2']| by A1, FINSEQ_1:98; :: according to SPPOL_2:def 1 :: thesis: ex f1, f2 being S-Sequence_in_R2 st
( |[r1,r1']| = f1 /. 1 & |[r1,r1']| = f2 /. 1 & |[r2,r2']| = f1 /. (len f1) & |[r2,r2']| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r1']|,|[r2,r2']|} & [.r1,r2,r1',r2'.] = (L~ f1) \/ (L~ f2) )
A3: ( |[r1,r1']| `1 = r1 & |[r1,r1']| `2 = r1' & |[r1,r2']| `1 = r1 & |[r1,r2']| `2 = r2' & |[r2,r2']| `1 = r2 & |[r2,r2']| `2 = r2' & |[r2,r1']| `1 = r2 & |[r2,r1']| `2 = r1' ) by EUCLID:56;
set f1 = <*|[r1,r1']|,|[r1,r2']|,|[r2,r2']|*>;
set f2 = <*|[r1,r1']|,|[r2,r1']|,|[r2,r2']|*>;
A4: ( len <*|[r1,r1']|,|[r1,r2']|,|[r2,r2']|*> = 3 & len <*|[r1,r1']|,|[r2,r1']|,|[r2,r2']|*> = 3 ) by FINSEQ_1:62;
reconsider f1 = <*|[r1,r1']|,|[r1,r2']|,|[r2,r2']|*>, f2 = <*|[r1,r1']|,|[r2,r1']|,|[r2,r2']|*> as S-Sequence_in_R2 by A1, A2, A3, TOPREAL3:41, TOPREAL3:42;
take f1 ; :: thesis: ex f2 being S-Sequence_in_R2 st
( |[r1,r1']| = f1 /. 1 & |[r1,r1']| = f2 /. 1 & |[r2,r2']| = f1 /. (len f1) & |[r2,r2']| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r1']|,|[r2,r2']|} & [.r1,r2,r1',r2'.] = (L~ f1) \/ (L~ f2) )
take f2 ; :: thesis: ( |[r1,r1']| = f1 /. 1 & |[r1,r1']| = f2 /. 1 & |[r2,r2']| = f1 /. (len f1) & |[r2,r2']| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r1']|,|[r2,r2']|} & [.r1,r2,r1',r2'.] = (L~ f1) \/ (L~ f2) )
thus ( |[r1,r1']| = f1 /. 1 & |[r1,r1']| = f2 /. 1 & |[r2,r2']| = f1 /. (len f1) & |[r2,r2']| = f2 /. (len f2) ) by A4, FINSEQ_4:27; :: thesis: ( (L~ f1) /\ (L~ f2) = {|[r1,r1']|,|[r2,r2']|} & [.r1,r2,r1',r2'.] = (L~ f1) \/ (L~ f2) )
A5: L~ f1 = (LSeg |[r1,r1']|,|[r1,r2']|) \/ (LSeg |[r1,r2']|,|[r2,r2']|) by TOPREAL3:23;
A6: L~ f2 = (LSeg |[r2,r2']|,|[r2,r1']|) \/ (LSeg |[r2,r1']|,|[r1,r1']|) by TOPREAL3:23;
hence (L~ f1) /\ (L~ f2) = (((LSeg |[r1,r1']|,|[r1,r2']|) \/ (LSeg |[r1,r2']|,|[r2,r2']|)) /\ (LSeg |[r2,r2']|,|[r2,r1']|)) \/ (((LSeg |[r1,r1']|,|[r1,r2']|) \/ (LSeg |[r1,r2']|,|[r2,r2']|)) /\ (LSeg |[r2,r1']|,|[r1,r1']|)) by A5, XBOOLE_1:23
.= (((LSeg |[r1,r2']|,|[r1,r1']|) \/ (LSeg |[r2,r2']|,|[r1,r2']|)) /\ (LSeg |[r2,r1']|,|[r2,r2']|)) \/ {|[r1,r1']|} by A2, A3, TOPREAL3:34
.= {|[r2,r2']|} \/ {|[r1,r1']|} by A1, A3, TOPREAL3:35
.= {|[r1,r1']|,|[r2,r2']|} by ENUMSET1:41 ;
:: thesis: [.r1,r2,r1',r2'.] = (L~ f1) \/ (L~ f2)
thus [.r1,r2,r1',r2'.] = (L~ f1) \/ (L~ f2) by A6, TOPREAL3:23; :: thesis: verum