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

now

let x be set ; :: 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