per cases ( X is empty or not X is empty ) ;
suppose A1: X is empty ; :: thesis: (id X) . x = x
then x is empty by SUBSET_1:def 1;
hence (id X) . x = x by A1; :: thesis: verum
end;
suppose not X is empty ; :: thesis: (id X) . x = x
hence (id X) . x = x by Th18; :: thesis: verum
end;
end;