set p = |[0,0]|;

set q = |[1,1]|;

set f = <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*>;

A1: |[0,0]| `2 = 0 by EUCLID:52;

A2: |[1,1]| `1 = 1 by EUCLID:52;

A3: |[1,1]| `2 = 1 by EUCLID:52;

|[0,0]| `1 = 0 by EUCLID:52;

then <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-Seq by A1, A2, A3, TOPREAL3:34;

then L~ <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-P_arc ;

hence ex b_{1} being Subset of (TOP-REAL 2) st b_{1} is being_S-P_arc
; :: thesis: verum

set q = |[1,1]|;

set f = <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*>;

A1: |[0,0]| `2 = 0 by EUCLID:52;

A2: |[1,1]| `1 = 1 by EUCLID:52;

A3: |[1,1]| `2 = 1 by EUCLID:52;

|[0,0]| `1 = 0 by EUCLID:52;

then <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-Seq by A1, A2, A3, TOPREAL3:34;

then L~ <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-P_arc ;

hence ex b