set e = {} ;
reconsider e = {} as preProgram of S by FUNCT_1:174, RELAT_1:206;
take e ; :: thesis: e is initial
thus e is initial ; :: thesis: verum