let A, B be set ; :: thesis: for R being Subset of [:A,B:] holds rng (.: ) c= bool (rng R)
let R be Subset of [:A,B:]; :: thesis: rng (.: ) c= bool (rng R)
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (.: ) or y in bool (rng R) )
reconsider yy = y as set by TARSKI:1;
assume y in rng (.: ) ; :: thesis: y in bool (rng R)
then consider x being object such that
A1: x in dom (.: ) and
A2: y = (.: ) . x by FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
y = R .: x by A1, A2, Th19;
then yy c= rng R by RELAT_1:111;
hence y in bool (rng R) ; :: thesis: verum