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:136;
Big is subset-closed by A2, Def1;
then A5: Big is Tarski by A3, Def2;
defpred S₁[ set ] means $1 is_Tarski-Class_of A;
consider Classes being set such that
A6: for X being set holds
( X in Classes iff ( X in bool Big & S₁[X] ) ) from XBOOLE_0:sch 1();
set IT = meet Classes;
A7: ( Big in bool Big & Big is_Tarski-Class_of A ) by A1, A5, Def3, ZFMISC_1:def 1;
then A8: Big in Classes by A6;
A9: Classes <> {} by A6, A7;

A10: now

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

end;

then A13: A in meet Classes by A9, SETFAM_1:def 1;
take meet Classes ; :: thesis:
thus A in meet Classes by A9, A10, SETFAM_1:def 1; :: according to CLASSES1:def 3 :: thesis:
thus A14: 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
A15: X in meet Classes and
A16: Y c= X ; :: thesis:

let Z be set ; :: thesis:
assume A18: Z in Classes ; :: thesis:
then Z is_Tarski-Class_of A by A6;
then Z is Tarski by Def3;
then A21: Z is subset-closed by Def2;
X in Z by A15, A18, SETFAM_1:def 1;
hence Y in Z by A16, A21, Def1; :: thesis:

end;

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

end;

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

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

let Z be set ; :: thesis:
assume A26: Z in Classes ; :: thesis:
then Z is_Tarski-Class_of A by A6;
then A28: Z is Tarski by Def3;
X in Z by A24, A26, SETFAM_1:def 1;
hence bool X in Z by A28, Def2; :: thesis:

end;

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

end;

thus A30: 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
A31: X c= meet Classes and
A32: not X, meet Classes are_equipotent ; :: thesis:

let Z be set ; :: thesis:
assume A34: Z in Classes ; :: thesis:
then Z is_Tarski-Class_of A by A6;
then A36: Z is Tarski by Def3;
A37: meet Classes c= Z by A34, SETFAM_1:4;
then X c= Z by A31, XBOOLE_1:1;
then ( X,Z are_equipotent or X in Z ) by A36, Def2;
hence X in Z by A31, A32, A37, CARD_1:44; :: thesis:

end;

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

end;

let D be set ; :: thesis:
assume A40: D is_Tarski-Class_of A ; :: thesis:
then A41: A in D by Def3;
A42: D is Tarski by A40, Def3;
then A43: D is subset-closed by Def2;
A44: (meet Classes) /\ D is_Tarski-Class_of A

thus A in (meet Classes) /\ D by A13, A41, 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
A45: X in (meet Classes) /\ D and
A46: Y c= X ; :: thesis:
A47: X in meet Classes by A45, XBOOLE_0:def 4;
A48: X in D by A45, XBOOLE_0:def 4;
A49: Y in meet Classes by A14, A46, A47;
Y in D by A43, A46, A48, Def1;
hence Y in (meet Classes) /\ D by A49, 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 A51: X in (meet Classes) /\ D ; :: thesis:
then A52: X in meet Classes by XBOOLE_0:def 4;
A53: X in D by A51, XBOOLE_0:def 4;
A54: bool X in meet Classes by A23, A52;
bool X in D by A42, A53, Def2;
hence bool X in (meet Classes) /\ D by A54, XBOOLE_0:def 4; :: thesis:

end;

let X be set ; :: thesis:
assume that
A56: X c= (meet Classes) /\ D and
A57: not X,(meet Classes) /\ D are_equipotent ; :: thesis:
A58: (meet Classes) /\ D c= meet Classes by XBOOLE_1:17;
A59: (meet Classes) /\ D c= D by XBOOLE_1:17;
A60: not X, meet Classes are_equipotent by A56, A57, A58, CARD_1:44;
A61: ( X c= D & not X,D are_equipotent ) by A56, A57, A59, CARD_1:44, XBOOLE_1:1;
A62: X in meet Classes by A30, A56, A58, A60, XBOOLE_1:1;
X in D by A42, A61, Def2;
hence X in (meet Classes) /\ D by A62, XBOOLE_0:def 4; :: thesis:

end;

(meet Classes) /\ D c= Big

let x be set ; :: 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 A8, SETFAM_1:def 1; :: thesis:

end;

then (meet Classes) /\ D in Classes by A6, A44;
then A68: meet Classes c= (meet Classes) /\ D by SETFAM_1:4;
(meet Classes) /\ D c= D by XBOOLE_1:17;
hence meet Classes c= D by A68, XBOOLE_1:1; :: thesis: