let D be set ; :: thesis: for SD being Subset-Family of D holds
( SD = { y where y is Subset of D : y is finite } iff SD = Fin D )
let SD be Subset-Family of D; :: thesis: ( SD = { y where y is Subset of D : y is finite } iff SD = Fin D )
thus ( SD = { y where y is Subset of D : y is finite } implies SD = Fin D ) :: thesis: ( SD = Fin D implies SD = { y where y is Subset of D : y is finite } )

proof

assume A1: SD = { y where y is Subset of D : y is finite } ; :: thesis: SD = Fin D
thus SD c= Fin D :: according to XBOOLE_0:def 10 :: thesis: Fin D c= SD

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SD or x in Fin D )
assume x in SD ; :: thesis: x in Fin D
then ex y being Subset of D st
( x = y & y is finite ) by A1;
hence x in Fin D by FINSUB_1:def 5; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Fin D or x in SD )
assume B1: x in Fin D ; :: thesis: x in SD
reconsider x = x as set by TARSKI:1;
( x c= D & x is finite ) by B1, FINSUB_1:def 5;
hence x in SD by A1; :: thesis: verum

end;

for D being set
for SD being Subset-Family of D st SD = Fin D holds
SD = { y where y is Subset of D : y is finite }

proof

let D be set ; :: thesis: for SD being Subset-Family of D st SD = Fin D holds
SD = { y where y is Subset of D : y is finite }
let SD be Subset-Family of D; :: thesis: ( SD = Fin D implies SD = { y where y is Subset of D : y is finite } )
assume A4: SD = Fin D ; :: thesis: SD = { y where y is Subset of D : y is finite }
then A5: SD c= { y where y is Subset of D : y is finite } ;
{ y where y is Subset of D : y is finite } c= SD

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { y where y is Subset of D : y is finite } or x in SD )
assume x in { y where y is Subset of D : y is finite } ; :: thesis: x in SD
then consider y being Subset of D such that
A6: ( x = y & y is finite ) ;
thus x in SD by A4, A6, FINSUB_1:def 5; :: thesis: verum

end;

hence SD = { y where y is Subset of D : y is finite } by A5; :: thesis: verum

end;

hence ( SD = Fin D implies SD = { y where y is Subset of D : y is finite } ) ; :: thesis: verum