let X be set ; :: thesis: for n being Nat holds
( (sequence_univers X) . (n + 1) is epsilon-transitive & Tarski-Class ((sequence_univers X) . (n + 1)) = GrothendieckUniverse ((sequence_univers X) . (n + 1)) )
let n be Nat; :: thesis: ( (sequence_univers X) . (n + 1) is epsilon-transitive & Tarski-Class ((sequence_univers X) . (n + 1)) = GrothendieckUniverse ((sequence_univers X) . (n + 1)) )
(sequence_univers X) . (n + 1) = GrothendieckUniverse ((sequence_univers X) . n) by Def9;
hence ( (sequence_univers X) . (n + 1) is epsilon-transitive & Tarski-Class ((sequence_univers X) . (n + 1)) = GrothendieckUniverse ((sequence_univers X) . (n + 1)) ) by CLASSES3:22; :: thesis: verum