for X being non empty TopStruct
for a, b being Point of X
for P being Path of a,b st P . 0 = a & P . 1 = b holds
( (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a )