let T be set ; :: thesis: for F being Subset-Family of T holds F = { B where B is Subset of T : B in F }
let F be Subset-Family of T; :: thesis: F = { B where B is Subset of T : B in F }
A1: F c= { B where B is Subset of T : B in F } ;
{ B where B is Subset of T : B in F } c= F

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of T : B in F } or x in F )
assume x in { B where B is Subset of T : B in F } ; :: thesis: x in F
then ex B being Subset of T st
( x = B & B in F ) ;
hence x in F ; :: thesis: verum

end;

hence F = { B where B is Subset of T : B in F } by A1; :: thesis: verum