let U be Grothendieck; :: thesis: U is Tarski
thus U is subset-closed ; :: according to CLASSES1:def 2 :: thesis: ( ( for b₁ being set holds
( not b₁ in U or bool b₁ in U ) ) & ( for b₁ being set holds
( not b₁ c= U or b₁,U are_equipotent or b₁ in U ) ) )
thus for X being set st X in U holds
bool X in U by Def1; :: thesis: for b₁ being set holds
( not b₁ c= U or b₁,U are_equipotent or b₁ 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: X,U are_equipotent
then consider f being Function such that
A2: ( f is one-to-one & dom f = On U & rng f = X ) by A1, Th16;
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 A2, FUNCT_1:33;
then ( dom (g * (f ")) = X & rng (g * (f ")) = U ) by A3, RELAT_1:27, RELAT_1:28;
hence X,U are_equipotent by A2, A3, WELLORD2:def 4; :: thesis: verum

end;

hence ( X,U are_equipotent or X in U ) ; :: thesis: verum