let A, B be set ; :: thesis: for X being Subset of A
for R being Relation of A,B holds R .: X = union { (Class (R,x)) where x is Element of A : x in X }
let X be Subset of A; :: thesis: for R being Relation of A,B holds R .: X = union { (Class (R,x)) where x is Element of A : x in X }
let R be Relation of A,B; :: thesis: R .: X = union { (Class (R,x)) where x is Element of A : x in X }
thus R .: X c= union { (Class (R,x)) where x is Element of A : x in X } :: according to XBOOLE_0:def 10 :: thesis: union { (Class (R,x)) where x is Element of A : x in X } c= R .: X

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: X or y in union { (Class (R,x)) where x is Element of A : x in X } )
assume y in R .: X ; :: thesis: y in union { (Class (R,x)) where x is Element of A : x in X }
then consider x1 being object such that
A1: [x1,y] in R and
A2: x1 in X by RELAT_1:def 13;
x1 in union { {x} where x is Element of A : x in X } by A2, Th15;
then consider S being set such that
A3: x1 in S and
A4: S in { {x} where x is Element of A : x in X } by TARSKI:def 4;
consider x being Element of A such that
A5: S = {x} and
A6: x in X by A4;
A7: y in R .: {x} by A1, A3, A5, RELAT_1:def 13;
set Y = R .: {x};
R .: {x} = Class (R,x) ;
then R .: {x} in { (Class (R,xs)) where xs is Element of A : xs in X } by A6;
hence y in union { (Class (R,x)) where x is Element of A : x in X } by A7, TARSKI:def 4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union { (Class (R,x)) where x is Element of A : x in X } or a in R .: X )
assume a in union { (Class (R,x)) where x is Element of A : x in X } ; :: thesis: a in R .: X
then consider Y being set such that
A8: a in Y and
A9: Y in { (Class (R,x)) where x is Element of A : x in X } by TARSKI:def 4;
consider x being Element of A such that
A10: Y = Class (R,x) and
A11: x in X by A9;
Y c= R .: X

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in Y or b in R .: X )
assume b in Y ; :: thesis: b in R .: X
then consider x1 being object such that
A12: [x1,b] in R and
A13: x1 in {x} by A10, RELAT_1:def 13;
x1 = x by A13, TARSKI:def 1;
hence b in R .: X by A11, A12, RELAT_1:def 13; :: thesis: verum

end;

hence a in R .: X by A8; :: thesis: verum