set p = |[0 ,0 ]|;
set q = |[1,1]|;
set f = <*|[0 ,0 ]|,|[(|[0 ,0 ]| `1 ),(|[1,1]| `2 )]|,|[1,1]|*>;
( 0 <> 1 & |[0 ,0 ]| `1 = 0 & |[0 ,0 ]| `2 = 0 & |[1,1]| `1 = 1 & |[1,1]| `2 = 1 ) by EUCLID:56;
then <*|[0 ,0 ]|,|[(|[0 ,0 ]| `1 ),(|[1,1]| `2 )]|,|[1,1]|*> is being_S-Seq by TOPREAL3:41;
then L~ <*|[0 ,0 ]|,|[(|[0 ,0 ]| `1 ),(|[1,1]| `2 )]|,|[1,1]|*> is being_S-P_arc by TOPREAL1:def 11;
hence ex b₁ being Subset of (TOP-REAL 2) st b₁ is being_S-P_arc ; :: thesis: verum