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

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

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,B:] or a in (id A) | B )
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;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

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