let X be set ; :: thesis: for A being Subset of X holds (id X) .: A = A
let A be Subset of X; :: thesis: (id X) .: A = A
now :: thesis: for e being object holds
( ( e in A implies ex u being object st
( u in dom (id X) & u in A & e = (id X) . u ) ) & ( ex u being object st
( u in dom (id X) & u in A & e = (id X) . u ) implies e in A ) )
let e be object ; :: thesis: ( ( e in A implies ex u being object st
( u in dom (id X) & u in A & e = (id X) . u ) ) & ( ex u being object st
( u in dom (id X) & u in A & e = (id X) . u ) implies e in A ) )
thus ( e in A implies ex u being object st
( u in dom (id X) & u in A & e = (id X) . u ) ) :: thesis: ( ex u being object st
( u in dom (id X) & u in A & e = (id X) . u ) implies e in A )
proof
assume A1: e in A ; :: thesis: ex u being object st
( u in dom (id X) & u in A & e = (id X) . u )
take e ; :: thesis: ( e in dom (id X) & e in A & e = (id X) . e )
thus e in dom (id X) by A1; :: thesis: ( e in A & e = (id X) . e )
thus e in A by A1; :: thesis: e = (id X) . e
thus e = (id X) . e by A1, Th17; :: thesis: verum
end;
assume ex u being object st
( u in dom (id X) & u in A & e = (id X) . u ) ; :: thesis: e in A
hence e in A by Th17; :: thesis: verum
end;
hence (id X) .: A = A by Def6; :: thesis: verum