let A, B be set ; :: thesis: ( B c= A implies (id A) .: B = B )
assume A1: B c= A ; :: thesis: (id A) .: B = B
A2: dom (id A) = A by FUNCT_1:34;
thus (id A) .: B c= B :: according to XBOOLE_0:def 10 :: thesis: B c= (id A) .: B

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in (id A) .: B or y in B )
assume y in (id A) .: B ; :: thesis: y in B
then consider x being set such that
A3: x in dom (id A) and
A4: x in B and
A5: (id A) . x = y by FUNCT_1:def 12;
thus y in B by A3, A4, A5, FUNCT_1:34; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in B or y in (id A) .: B )
assume A6: y in B ; :: thesis: y in (id A) .: B
then (id A) . y = y by A1, FUNCT_1:34;
hence y in (id A) .: B by A1, A2, A6, FUNCT_1:def 12; :: thesis: verum