let S be non empty RelStr ; :: thesis: for D being non empty Subset of S holds D = { i where i is Element of S : i in D }
let D be non empty Subset of S; :: thesis: D = { i where i is Element of S : i in D }
thus D c= { i where i is Element of S : i in D } ; :: according to XBOOLE_0:def 10 :: thesis: { i where i is Element of S : i in D } c= D
thus { i where i is Element of S : i in D } c= D :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { i where i is Element of S : i in D } or a in D )
assume a in { i where i is Element of S : i in D } ; :: thesis: a in D
then ex j being Element of S st
( j = a & j in D ) ;
hence a in D ; :: thesis: verum

end;