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

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