let U be Universe; :: thesis: for X being finite Subset of U holds X in U
let X be finite Subset of U; :: thesis: X in U

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: X in U

hence X in U by CLASSES2:56; :: thesis: verum

end;

suppose not X is empty ; :: thesis: X in U

then reconsider X = X as non empty set ;
reconsider Y = SmallestPartition X as non empty set ;
consider p being FinSequence such that
A1: rng p = Y and
p is one-to-one by FINSEQ_4:58;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
A0: Y = { {x} where x is Element of X : verum } by EQREL_1:37;

now :: thesis: for o being object st o in Y holds
o in U

let o be object ; :: thesis: ( o in Y implies o in U )
assume o in Y ; :: thesis: o in U
then consider x being Element of X such that
A3: o = {x} by A0;
( x in X & X c= U ) ;
hence o in U by A3, Th18; :: thesis: verum

end;

then rng p c= U by A1;
then union (rng p) in U by A2, CLASSES4:5, CLASSES4:57;
hence X in U by A1, Th7; :: thesis: verum

end;

end;