let X be set ; :: thesis: sequence_univers X is Sequence
sequence_univers X is Sequence-like by Def9;
hence sequence_univers X is Sequence ; :: thesis: verum