let T be TopStruct ; :: thesis: {} is Curve of T
reconsider f = {} as parametrized-curve PartFunc of R^1,T by Lm1, XBOOLE_1:2;
f is Curve of T by Th20;
hence {} is Curve of T ; :: thesis: verum