let x be object ; :: thesis: ( x is Set of FinSETS iff x is FinSet )

hereby :: thesis: ( x is FinSet implies x is Set of FinSETS )

assume x is Set of FinSETS ; :: thesis: x is FinSet
then x is FinSETS -set by Def10;
hence x is FinSet ; :: thesis: verum

end;

assume x is FinSet ; :: thesis: x is Set of FinSETS
then x is FinSETS -set ;
hence x is Set of FinSETS by Def10; :: thesis: verum