let I be set ; :: thesis: {} is Element of Fin I
A1: Fin {} c= Fin I by XBOOLE_1:2, FINSUB_1:10;
{} in {{}} by TARSKI:def 1;
hence {} is Element of Fin I by A1, FINSUB_1:15; :: thesis: verum