let X be set ; :: thesis: for S being Subset-Family of X holds <.S.] = { x where x is Subset of X : ex b being Element of S st b c= x }
let S be Subset-Family of X; :: thesis: <.S.] = { x where x is Subset of X : ex b being Element of S st b c= x }
set SX = { x where x is Subset of X : ex b being Element of S st b c= x } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { x where x is Subset of X : ex b being Element of S st b c= x } c= <.S.]

let x be object ; :: thesis: ( x in <.S.] implies x in { x where x is Subset of X : ex b being Element of S st b c= x } )
assume A1: x in <.S.] ; :: thesis: x in { x where x is Subset of X : ex b being Element of S st b c= x }
then reconsider x1 = x as Subset of X ;
ex b being Element of S st b c= x1 by A1, def3;
hence x in { x where x is Subset of X : ex b being Element of S st b c= x } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Subset of X : ex b being Element of S st b c= x } or x in <.S.] )
assume x in { x where x is Subset of X : ex b being Element of S st b c= x } ; :: thesis: x in <.S.]
then consider x0 being Subset of X such that
A2: x = x0 and
A3: ex b being Element of S st b c= x0 ;
reconsider x1 = x as Subset of X by A2;
thus x in <.S.] by A2, A3, def3; :: thesis: verum