let P be Subset of (TOP-REAL 2); :: thesis: for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds

p2,p1 split P

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1,p2 split P implies p2,p1 split P )

assume A1: p1 <> p2 ; :: according to SPPOL_2:def 1 :: thesis: ( for f1, f2 being S-Sequence_in_R2 holds

( not p1 = f1 /. 1 or not p1 = f2 /. 1 or not p2 = f1 /. (len f1) or not p2 = f2 /. (len f2) or not (L~ f1) /\ (L~ f2) = {p1,p2} or not P = (L~ f1) \/ (L~ f2) ) or p2,p1 split P )

given f1, f2 being S-Sequence_in_R2 such that A2: p1 = f1 /. 1 and

A3: p1 = f2 /. 1 and

A4: p2 = f1 /. (len f1) and

A5: p2 = f2 /. (len f2) and

A6: (L~ f1) /\ (L~ f2) = {p1,p2} and

A7: P = (L~ f1) \/ (L~ f2) ; :: thesis: p2,p1 split P

thus p2 <> p1 by A1; :: according to SPPOL_2:def 1 :: thesis: ex f1, f2 being S-Sequence_in_R2 st

( p2 = f1 /. 1 & p2 = f2 /. 1 & p1 = f1 /. (len f1) & p1 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p2,p1} & P = (L~ f1) \/ (L~ f2) )

reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2 ;

take g1 ; :: thesis: ex f2 being S-Sequence_in_R2 st

( p2 = g1 /. 1 & p2 = f2 /. 1 & p1 = g1 /. (len g1) & p1 = f2 /. (len f2) & (L~ g1) /\ (L~ f2) = {p2,p1} & P = (L~ g1) \/ (L~ f2) )

take g2 ; :: thesis: ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) )

A8: len g2 = len f2 by FINSEQ_5:def 3;

len g1 = len f1 by FINSEQ_5:def 3;

hence ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) ) by A2, A3, A4, A5, A8, FINSEQ_5:65; :: thesis: ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) )

L~ g1 = L~ f1 by Th22;

hence ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) ) by A6, A7, Th22; :: thesis: verum

p2,p1 split P

let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( p1,p2 split P implies p2,p1 split P )

assume A1: p1 <> p2 ; :: according to SPPOL_2:def 1 :: thesis: ( for f1, f2 being S-Sequence_in_R2 holds

( not p1 = f1 /. 1 or not p1 = f2 /. 1 or not p2 = f1 /. (len f1) or not p2 = f2 /. (len f2) or not (L~ f1) /\ (L~ f2) = {p1,p2} or not P = (L~ f1) \/ (L~ f2) ) or p2,p1 split P )

given f1, f2 being S-Sequence_in_R2 such that A2: p1 = f1 /. 1 and

A3: p1 = f2 /. 1 and

A4: p2 = f1 /. (len f1) and

A5: p2 = f2 /. (len f2) and

A6: (L~ f1) /\ (L~ f2) = {p1,p2} and

A7: P = (L~ f1) \/ (L~ f2) ; :: thesis: p2,p1 split P

thus p2 <> p1 by A1; :: according to SPPOL_2:def 1 :: thesis: ex f1, f2 being S-Sequence_in_R2 st

( p2 = f1 /. 1 & p2 = f2 /. 1 & p1 = f1 /. (len f1) & p1 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p2,p1} & P = (L~ f1) \/ (L~ f2) )

reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2 ;

take g1 ; :: thesis: ex f2 being S-Sequence_in_R2 st

( p2 = g1 /. 1 & p2 = f2 /. 1 & p1 = g1 /. (len g1) & p1 = f2 /. (len f2) & (L~ g1) /\ (L~ f2) = {p2,p1} & P = (L~ g1) \/ (L~ f2) )

take g2 ; :: thesis: ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) )

A8: len g2 = len f2 by FINSEQ_5:def 3;

len g1 = len f1 by FINSEQ_5:def 3;

hence ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) ) by A2, A3, A4, A5, A8, FINSEQ_5:65; :: thesis: ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) )

L~ g1 = L~ f1 by Th22;

hence ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) ) by A6, A7, Th22; :: thesis: verum