consider Big being set such that
A1: A in Big and
A2: for X, Y being set st X in Big & Y c= X holds
Y in Big and
A3: ( ( for X being set st X in Big holds
bool X in Big ) & ( for X being set holds
( not X c= Big or X,Big are_equipotent or X in Big ) ) ) by ZFMISC_1:112;
A4: Big is Tarski by A3, A2, Def1;
defpred S₁[ set ] means $1 is_Tarski-Class_of A;
consider Classes being set such that
A5: for X being set holds
( X in Classes iff ( X in bool Big & S₁[X] ) ) from XFAMILY:sch 1();
set IT = meet Classes;
A6: ( Big in bool Big & Big is_Tarski-Class_of A ) by A1, A4, ZFMISC_1:def 1;
then A7: Big in Classes by A5;
A8: Classes <> {} by A5, A6;

A9: now :: thesis:

let X be set ; :: thesis:
assume X in Classes ; :: thesis:
then X is_Tarski-Class_of A by A5;
hence A in X ; :: thesis:

end;

then A10: A in meet Classes by A8, SETFAM_1:def 1;
take meet Classes ; :: thesis:
thus A in meet Classes by A8, A9, SETFAM_1:def 1; :: according to CLASSES1:def 3 :: thesis:
thus A11: for X, Y being set st X in meet Classes & Y c= X holds
Y in meet Classes :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis:

let X, Y be set ; :: thesis:
assume that
A12: X in meet Classes and
A13: Y c= X ; :: thesis:

let Z be set ; :: thesis:
assume A14: Z in Classes ; :: thesis:
then Z is_Tarski-Class_of A by A5;
then Z is Tarski ;
then A15: Z is subset-closed ;
X in Z by A12, A14, SETFAM_1:def 1;
hence Y in Z by A13, A15; :: thesis:

end;

hence Y in meet Classes by A8, SETFAM_1:def 1; :: thesis:

end;

thus A16: for X being set st X in meet Classes holds
bool X in meet Classes :: thesis:

let X be set ; :: thesis:
assume A17: X in meet Classes ; :: thesis:

let Z be set ; :: thesis:
assume A18: Z in Classes ; :: thesis:
then Z is_Tarski-Class_of A by A5;
then A19: Z is Tarski ;
X in Z by A17, A18, SETFAM_1:def 1;
hence bool X in Z by A19; :: thesis:

end;

hence bool X in meet Classes by A8, SETFAM_1:def 1; :: thesis:

end;

thus A20: for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) :: thesis:

let X be set ; :: thesis:
assume that
A21: X c= meet Classes and
A22: not X, meet Classes are_equipotent ; :: thesis:

let Z be set ; :: thesis:
assume A23: Z in Classes ; :: thesis:
then Z is_Tarski-Class_of A by A5;
then A24: Z is Tarski ;
A25: meet Classes c= Z by A23, SETFAM_1:3;
then X c= Z by A21;
then ( X,Z are_equipotent or X in Z ) by A24;
hence X in Z by A21, A22, A25, CARD_1:24; :: thesis:

end;

hence X in meet Classes by A8, SETFAM_1:def 1; :: thesis:

end;

let D be set ; :: thesis:
assume A26: D is_Tarski-Class_of A ; :: thesis:
then A27: A in D ;
A28: D is Tarski by A26;
then A29: D is subset-closed ;
A30: (meet Classes) /\ D is_Tarski-Class_of A

thus A in (meet Classes) /\ D by A10, A27, XBOOLE_0:def 4; :: according to CLASSES1:def 3 :: thesis:
thus for X, Y being set st X in (meet Classes) /\ D & Y c= X holds
Y in (meet Classes) /\ D :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis:

let X, Y be set ; :: thesis:
assume that
A31: X in (meet Classes) /\ D and
A32: Y c= X ; :: thesis:
A33: X in meet Classes by A31, XBOOLE_0:def 4;
A34: X in D by A31, XBOOLE_0:def 4;
A35: Y in meet Classes by A11, A32, A33;
Y in D by A29, A32, A34;
hence Y in (meet Classes) /\ D by A35, XBOOLE_0:def 4; :: thesis:

end;

thus for X being set st X in (meet Classes) /\ D holds
bool X in (meet Classes) /\ D :: thesis:

let X be set ; :: thesis:
assume A36: X in (meet Classes) /\ D ; :: thesis:
then A37: X in meet Classes by XBOOLE_0:def 4;
A38: X in D by A36, XBOOLE_0:def 4;
A39: bool X in meet Classes by A16, A37;
bool X in D by A28, A38;
hence bool X in (meet Classes) /\ D by A39, XBOOLE_0:def 4; :: thesis:

end;

let X be set ; :: thesis:
assume that
A40: X c= (meet Classes) /\ D and
A41: not X,(meet Classes) /\ D are_equipotent ; :: thesis:
A42: (meet Classes) /\ D c= meet Classes by XBOOLE_1:17;
A43: (meet Classes) /\ D c= D by XBOOLE_1:17;
A44: not X, meet Classes are_equipotent by A40, A41, A42, CARD_1:24;
A45: ( X c= D & not X,D are_equipotent ) by A40, A41, A43, CARD_1:24;
A46: X in meet Classes by A20, A40, A42, A44, XBOOLE_1:1;
X in D by A28, A45;
hence X in (meet Classes) /\ D by A46, XBOOLE_0:def 4; :: thesis:

end;

(meet Classes) /\ D c= Big

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in (meet Classes) /\ D ; :: thesis:
then x in meet Classes by XBOOLE_0:def 4;
hence x in Big by A7, SETFAM_1:def 1; :: thesis:

end;

then A47: meet Classes c= (meet Classes) /\ D by SETFAM_1:3, A5, A30;
(meet Classes) /\ D c= D by XBOOLE_1:17;
hence meet Classes c= D by A47; :: thesis: