let X, Y be set ; :: thesis: (id X) .: Y c= Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (id X) .: Y or x in Y )
assume x in (id X) .: Y ; :: thesis: x in Y
then ex y being object st
( [y,x] in id X & y in Y ) by RELAT_1:def 13;
hence x in Y by RELAT_1:def 10; :: thesis: verum