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

proof

let y be object ; :: 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 ex x being object st
( x in dom (id A) & x in B & (id A) . x = y ) by FUNCT_1:def 6;
hence y in B by FUNCT_1:17; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in B or y in (id A) .: B )
assume A2: y in B ; :: thesis: y in (id A) .: B
then ( dom (id A) = A & (id A) . y = y ) by A1, FUNCT_1:17;
hence y in (id A) .: B by A1, A2, FUNCT_1:def 6; :: thesis: verum