set e = {} ;
{} is empty FinPartState of S by CARD_3:66;
then reconsider e = {} as preProgram of S ;
take e ; :: thesis: e is initial
thus e is initial ; :: thesis: verum