let X1 be non empty set ; :: thesis: for A1 being Subset of X1 holds A1 = { x1 where x1 is Element of X1 : x1 in A1 }
let A1 be Subset of X1; :: thesis: A1 = { x1 where x1 is Element of X1 : x1 in A1 }
thus A1 c= { x1 where x1 is Element of X1 : x1 in A1 } :: according to XBOOLE_0:def 10 :: thesis: { x1 where x1 is Element of X1 : x1 in A1 } c= A1

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A1 or a in { x1 where x1 is Element of X1 : x1 in A1 } )
assume a in A1 ; :: thesis: a in { x1 where x1 is Element of X1 : x1 in A1 }
hence a in { x1 where x1 is Element of X1 : x1 in A1 } ; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { x1 where x1 is Element of X1 : x1 in A1 } or a in A1 )
assume a in { x1 where x1 is Element of X1 : x1 in A1 } ; :: thesis: a in A1
then ex x1 being Element of X1 st
( a = x1 & x1 in A1 ) ;
hence a in A1 ; :: thesis: verum