let X, Y be set ; :: thesis: (id X) .: Y = X /\ Y
thus (id X) .: Y c= X /\ Y :: according to XBOOLE_0:def 10 :: thesis: X /\ Y c= (id X) .: Y

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (id X) .: Y or x in X /\ Y )
assume x in (id X) .: Y ; :: thesis: x in X /\ Y
then consider y being object such that
A1: ( [y,x] in id X & y in Y ) by RELAT_1:def 13;
( x = y & y in X ) by A1, RELAT_1:def 10;
hence x in X /\ Y by A1, XBOOLE_0:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ Y or x in (id X) .: Y )
assume x in X /\ Y ; :: thesis: x in (id X) .: Y
then A2: ( x in X & x in Y ) by XBOOLE_0:def 4;
then [x,x] in id X by RELAT_1:def 10;
hence x in (id X) .: Y by A2, RELAT_1:def 13; :: thesis: verum