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