set SF = { X where X is Subset of E : card X = n } ;

now :: thesis: for x being object st x in { X where X is Subset of E : card X = n } holds
x in bool E

let x be object ; :: thesis: ( x in { X where X is Subset of E : card X = n } implies x in bool E )
assume x in { X where X is Subset of E : card X = n } ; :: thesis: x in bool E
then ex X being Subset of E st
( X = x & card X = n ) ;
hence x in bool E ; :: thesis: verum

end;

hence { X where X is Subset of E : card X = n } is Subset-Family of E by TARSKI:def 3; :: thesis: verum