let U be Grothendieck; :: thesis: U is Tarski

thus U is subset-closed ; :: according to CLASSES1:def 2 :: thesis: ( ( for b_{1} being set holds

( not b_{1} in U or bool b_{1} in U ) ) & ( for b_{1} being set holds

( not b_{1} c= U or b_{1},U are_equipotent or b_{1} in U ) ) )

thus for X being set st X in U holds

bool X in U by Def1; :: thesis: for b_{1} being set holds

( not b_{1} c= U or b_{1},U are_equipotent or b_{1} 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 )

thus U is subset-closed ; :: according to CLASSES1:def 2 :: thesis: ( ( for b

( not b

( not b

thus for X being set st X in U holds

bool X in U by Def1; :: thesis: for b

( not b

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

hence
( X,U are_equipotent or X in U )
; :: thesis: verum
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;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