let c be Chain of G; :: thesis: c is empty
assume A1: not c is empty ; :: thesis: contradiction
c is FinSequence of the carrier' of G by Def1;
hence contradiction by A1; :: thesis: verum