theorem :: FVALUAT1:13

for D being non empty doubleLoopStr
for A being Subset of D holds A |^ 1 = A