let A, B be set ; :: thesis: (id A) | B = (id A) /\ [:B,B:]
thus (id A) | B c= (id A) /\ [:B,B:] :: according to XBOOLE_0:def 10 :: thesis: (id A) /\ [:B,B:] c= (id A) | B

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (id A) | B or a in (id A) /\ [:B,B:] )
assume A1: a in (id A) | B ; :: thesis: a in (id A) /\ [:B,B:]
(id A) | B is Relation of B,A by RELSET_1:33;
then consider x, y being set such that
A2: ( a = [x,y] & x in B & y in A ) by A1, RELSET_1:6;
A3: [x,y] in id A by A1, A2, RELAT_1:def 11;
then ( x in A & x = y ) by RELAT_1:def 10;
then [x,y] in [:B,B:] by A2, ZFMISC_1:106;
hence a in (id A) /\ [:B,B:] by A2, A3, XBOOLE_0:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (id A) /\ [:B,B:] or a in (id A) | B )
assume a in (id A) /\ [:B,B:] ; :: thesis: a in (id A) | B
then A4: ( a in id A & a in [:B,B:] ) by XBOOLE_0:def 4;
then consider x1, y1 being set such that
A5: ( x1 in B & y1 in B & a = [x1,y1] ) by ZFMISC_1:def 2;
thus a in (id A) | B by A4, A5, RELAT_1:def 11; :: thesis: verum