let A, B be set ; :: thesis: for X being Subset of A
for R being Subset of [:A,B:] st R = [:A,B:] holds
R .:^ X = B
let X be Subset of A; :: thesis: for R being Subset of [:A,B:] st R = [:A,B:] holds
R .:^ X = B
let R be Subset of [:A,B:]; :: thesis: ( R = [:A,B:] implies R .:^ X = B )
assume A1: R = [:A,B:] ; :: thesis: R .:^ X = B
thus R .:^ X c= B ; :: according to XBOOLE_0:def 10 :: thesis: B c= R .:^ X
thus B c= R .:^ X :: thesis: verum

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in R .:^ X )
assume A2: a in B ; :: thesis: a in R .:^ X
then reconsider B = B as non empty set ;
reconsider a = a as Element of B by A2;
for x being set st x in X holds
a in Im (R,x)

proof

let x be set ; :: thesis: ( x in X implies a in Im (R,x) )
assume x in X ; :: thesis: a in Im (R,x)
then [x,a] in R by A1, ZFMISC_1:87;
hence a in Im (R,x) by Th9; :: thesis: verum

end;

hence a in R .:^ X by Th25; :: thesis: verum

end;