let U be Grothendieck; :: thesis: U is Tarski
thus U is subset-closed ; :: according to CLASSES1:def 2 :: thesis: ( ( for b1 being set holds
( not b1 in U or bool b1 in U ) ) & ( for b1 being set holds
( not b1 c= U or b1,U are_equipotent or b1 in U ) ) )

thus for X being set st X in U holds
bool X in U by Def1; :: thesis: for b1 being set holds
( not b1 c= U or b1,U are_equipotent or b1 in U )

let X be set ; :: thesis: ( not X c= U or X,U are_equipotent or X in U )
assume A1: X c= U ; :: thesis: ( X,U are_equipotent or X in U )
( not X in U implies X,U are_equipotent )
proof
assume not X in U ; :: thesis:
then consider f being Function such that
A2: ( f is one-to-one & dom f = On U & rng f = X ) by ;
not U in U ;
then consider g being Function such that
A3: ( g is one-to-one & dom g = On U & rng g = U ) by Th16;
set gf = g * (f ");
( dom (f ") = X & rng (f ") = On U ) by ;
then ( dom (g * (f ")) = X & rng (g * (f ")) = U ) by ;
hence X,U are_equipotent by ; :: thesis: verum
end;
hence ( X,U are_equipotent or X in U ) ; :: thesis: verum