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;
A4: Big is subset-closed by A2, Def1;
A5: Big is Tarski by A3, A4, 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;
A8: Big in Classes by A6, A7;
A9: Classes <> {} by A6, A7;

A10: now

let X be set ; :: thesis: ( X in Classes implies A in X )
assume A11: X in Classes ; :: thesis: A in X
A12: X is_Tarski-Class_of A by A6, A11;
thus A in X by A12, Def3; :: thesis: verum

end;

A13: A in meet Classes by A9, A10, SETFAM_1:def 1;
take meet Classes ; :: thesis: ( meet Classes is_Tarski-Class_of A & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
thus A in meet Classes by A9, A10, SETFAM_1:def 1; :: according to CLASSES1:def 3 :: thesis: ( meet Classes is Tarski & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )
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: ( ( for X being set st X in meet Classes holds
bool X in meet Classes ) & ( for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) ) & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )

proof

let X, Y be set ; :: thesis: ( X in meet Classes & Y c= X implies Y in meet Classes )
assume that
A15: X in meet Classes and
A16: Y c= X ; :: thesis: Y in meet Classes

A17: now

let Z be set ; :: thesis: ( Z in Classes implies Y in Z )
assume A18: Z in Classes ; :: thesis: Y in Z
A19: Z is_Tarski-Class_of A by A6, A18;
A20: Z is Tarski by A19, Def3;
A21: Z is subset-closed by A20, Def2;
A22: X in Z by A15, A18, SETFAM_1:def 1;
thus Y in Z by A16, A21, A22, Def1; :: thesis: verum

end;

thus Y in meet Classes by A9, A17, SETFAM_1:def 1; :: thesis: verum

end;

thus A23: for X being set st X in meet Classes holds
bool X in meet Classes :: thesis: ( ( for X being set holds
( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes ) ) & ( for D being set st D is_Tarski-Class_of A holds
meet Classes c= D ) )

proof

let X be set ; :: thesis: ( X in meet Classes implies bool X in meet Classes )
assume A24: X in meet Classes ; :: thesis: bool X in meet Classes

A25: now

let Z be set ; :: thesis: ( Z in Classes implies bool X in Z )
assume A26: Z in Classes ; :: thesis: bool X in Z
A27: Z is_Tarski-Class_of A by A6, A26;
A28: Z is Tarski by A27, Def3;
A29: X in Z by A24, A26, SETFAM_1:def 1;
thus bool X in Z by A28, A29, Def2; :: thesis: verum

end;

thus bool X in meet Classes by A9, A25, SETFAM_1:def 1; :: thesis: verum

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: for D being set st D is_Tarski-Class_of A holds
meet Classes c= D

proof

let X be set ; :: thesis: ( not X c= meet Classes or X, meet Classes are_equipotent or X in meet Classes )
assume that
A31: X c= meet Classes and
A32: not X, meet Classes are_equipotent ; :: thesis: X in meet Classes

A33: now

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

end;

thus X in meet Classes by A9, A33, SETFAM_1:def 1; :: thesis: verum

end;

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

proof

thus A in (meet Classes) /\ D by A13, A41, XBOOLE_0:def 4; :: according to CLASSES1:def 3 :: thesis: (meet Classes) /\ D is Tarski
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: ( ( for X being set st X in (meet Classes) /\ D holds
bool X in (meet Classes) /\ D ) & ( for X being set holds
( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D ) ) )

proof

let X, Y be set ; :: thesis: ( X in (meet Classes) /\ D & Y c= X implies Y in (meet Classes) /\ D )
assume that
A45: X in (meet Classes) /\ D and
A46: Y c= X ; :: thesis: Y in (meet Classes) /\ D
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;
A50: Y in D by A43, A46, A48, Def1;
thus Y in (meet Classes) /\ D by A49, A50, XBOOLE_0:def 4; :: thesis: verum

end;

thus for X being set st X in (meet Classes) /\ D holds
bool X in (meet Classes) /\ D :: thesis: for X being set holds
( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D )

proof

let X be set ; :: thesis: ( X in (meet Classes) /\ D implies bool X in (meet Classes) /\ D )
assume A51: X in (meet Classes) /\ D ; :: thesis: bool X in (meet Classes) /\ D
A52: X in meet Classes by A51, XBOOLE_0:def 4;
A53: X in D by A51, XBOOLE_0:def 4;
A54: bool X in meet Classes by A23, A52;
A55: bool X in D by A42, A53, Def2;
thus bool X in (meet Classes) /\ D by A54, A55, XBOOLE_0:def 4; :: thesis: verum

end;

let X be set ; :: thesis: ( not X c= (meet Classes) /\ D or X,(meet Classes) /\ D are_equipotent or X in (meet Classes) /\ D )
assume that
A56: X c= (meet Classes) /\ D and
A57: not X,(meet Classes) /\ D are_equipotent ; :: thesis: X in (meet Classes) /\ D
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;
A63: X in D by A42, A61, Def2;
thus X in (meet Classes) /\ D by A62, A63, XBOOLE_0:def 4; :: thesis: verum

end;

A64: (meet Classes) /\ D c= Big

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (meet Classes) /\ D or x in Big )
assume A65: x in (meet Classes) /\ D ; :: thesis: x in Big
A66: x in meet Classes by A65, XBOOLE_0:def 4;
thus x in Big by A8, A66, SETFAM_1:def 1; :: thesis: verum

end;

A67: (meet Classes) /\ D in Classes by A6, A44, A64;
A68: meet Classes c= (meet Classes) /\ D by A67, SETFAM_1:4;
A69: (meet Classes) /\ D c= D by XBOOLE_1:17;
thus meet Classes c= D by A68, A69, XBOOLE_1:1; :: thesis: verum