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 object ; :: 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:18;
then consider x, y being object such that
A2: a = [x,y] and
A3: x in B and
y in A by A1, RELSET_1:2;
A4: [x,y] in id A by A1, A2, RELAT_1:def 11;
then x = y by RELAT_1:def 10;
then [x,y] in [:B,B:] by A3, ZFMISC_1:87;
hence a in (id A) /\ [:B,B:] by A2, A4, XBOOLE_0:def 4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (id A) /\ [:B,B:] or a in (id A) | B )
assume A5: a in (id A) /\ [:B,B:] ; :: thesis: a in (id A) | B
then a in [:B,B:] by XBOOLE_0:def 4;
then A6: ex x1, y1 being object st
( x1 in B & y1 in B & a = [x1,y1] ) by ZFMISC_1:def 2;
a in id A by A5, XBOOLE_0:def 4;
hence a in (id A) | B by A6, RELAT_1:def 11; :: thesis: verum