now :: thesis: ( c1 \/ c2 is not Curve of T implies {} is Curve of T )

assume c1 \/ c2 is not Curve of T ; :: thesis: {} is Curve of T
{} is parametrized-curve PartFunc of R^1,T by Lm1, XBOOLE_1:2;
hence {} is Curve of T by Th20; :: thesis: verum

end;

hence ( ( c1 \/ c2 is Curve of T implies c1 \/ c2 is Curve of T ) & ( c1 \/ c2 is not Curve of T implies {} is Curve of T ) & ( for b₁ being Curve of T holds verum ) ) ; :: thesis: verum