let x be object ; :: thesis: ex U being Universe st x is U -set
reconsider x = x as set by TARSKI:1;
take GrothendieckUniverse x ; :: thesis: x is GrothendieckUniverse x -set
thus x is GrothendieckUniverse x -set by CLASSES3:def 4; :: thesis: verum