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 & p1 = f2 /. 1 ) and
A3: ( p2 = f1 /. (len f1) & p2 = f2 /. (len f2) ) and
A4: (L~ f1) /\ (L~ f2) = {p1,p2} and
A5: 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 by Th47;
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) )
( len g1 = len f1 & len g2 = len f2 ) by FINSEQ_5:def 3;
hence ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) ) by A2, A3, FINSEQ_5:68; :: thesis: ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) )
( L~ g1 = L~ f1 & L~ g2 = L~ f2 ) by Th22;
hence ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) ) by A4, A5; :: thesis: verum