let Y be set ; :: thesis: for R being Relation holds (rng R) /\ Y c= (R ~ ) " (R " Y)
let R be Relation; :: thesis: (rng R) /\ Y c= (R ~ ) " (R " Y)
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (rng R) /\ Y or y in (R ~ ) " (R " Y) )
assume A1: y in (rng R) /\ Y ; :: thesis: y in (R ~ ) " (R " Y)
then y in rng R by XBOOLE_0:def 4;
then consider x being set such that
A2: [x,y] in R by Def5;
A3: [y,x] in R ~ by A2, Def7;
y in Y by A1, XBOOLE_0:def 4;
then x in R " Y by A2, Def14;
hence y in (R ~ ) " (R " Y) by A3, Def14; :: thesis: verum