set p = |[0,0]|;
set q = |[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;
hence
ex b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq
; verum