set F = { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ;
take D = meet { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ; :: thesis: ( A c= D & ( for x, y being set st [x,y] in D holds
x c= D ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
D c= B ) )
A1: A c= Rank (the_rank_of A) by CLASSES1:def 8;

A3: now

let x, y be set ; :: thesis: ( [x,y] in Rank (the_rank_of A) implies x c= Rank (the_rank_of A) )
assume [x,y] in Rank (the_rank_of A) ; :: thesis: x c= Rank (the_rank_of A)
then ( {x} in {{x,y},{x}} & {{x,y},{x}} c= Rank (the_rank_of A) ) by ORDINAL1:def 2, TARSKI:def 2;
then ( x in {x} & {x} c= Rank (the_rank_of A) ) by ORDINAL1:def 2, TARSKI:def 1;
hence x c= Rank (the_rank_of A) by ORDINAL1:def 2; :: thesis: verum

end;

Rank (the_rank_of A) c= Rank (the_rank_of A) ;
then A4: Rank (the_rank_of A) in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } by A1, A3;

hereby :: according to TARSKI:def 3 :: thesis: ( ( for x, y being set st [x,y] in D holds
x c= D ) & ( for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
D c= B ) )

let x be set ; :: thesis: ( x in A implies x in D )
assume A5: x in A ; :: thesis: x in D

now

let C be set ; :: thesis: ( C in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } implies x in C )
assume C in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ; :: thesis: x in C
then ex B being Subset of (Rank (the_rank_of A)) st
( C = B & A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) ) ;
hence x in C by A5; :: thesis: verum

end;

hence x in D by A4, SETFAM_1:def 1; :: thesis: verum

end;

hereby :: thesis: for B being set st A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) holds
D c= B

let x, y be set ; :: thesis: ( [x,y] in D implies x c= D )
assume A6: [x,y] in D ; :: thesis: x c= D
thus x c= D :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in x or z in D )
assume A7: z in x ; :: thesis: z in D

now

let X be set ; :: thesis: ( X in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } implies z in X )
assume X in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } ; :: thesis: z in X
then ( [x,y] in X & ex B being Subset of (Rank (the_rank_of A)) st
( X = B & A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) ) ) by A6, SETFAM_1:def 1;
then x c= X ;
hence z in X by A7; :: thesis: verum

end;

hence z in D by A4, SETFAM_1:def 1; :: thesis: verum

end;

end;

let B be set ; :: thesis: ( A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) implies D c= B )
assume A8: ( A c= B & ( for x, y being set st [x,y] in B holds
x c= B ) ) ; :: thesis: D c= B
set C = B /\ (Rank (the_rank_of A));
reconsider C = B /\ (Rank (the_rank_of A)) as Subset of (Rank (the_rank_of A)) by XBOOLE_1:17;
A9: A c= C by A1, A8, XBOOLE_1:19;

now

let x, y be set ; :: thesis: ( [x,y] in C implies x c= C )
assume [x,y] in C ; :: thesis: x c= C
then ( [x,y] in B & [x,y] in Rank (the_rank_of A) ) by XBOOLE_0:def 4;
then ( x c= B & x c= Rank (the_rank_of A) ) by A3, A8;
hence x c= C by XBOOLE_1:19; :: thesis: verum

end;

then C in { C where C is Subset of (Rank (the_rank_of A)) : ( A c= C & ( for x, y being set st [x,y] in C holds
x c= C ) ) } by A9;
then ( D c= C & C c= B ) by SETFAM_1:4, XBOOLE_1:17;
hence D c= B by XBOOLE_1:1; :: thesis: verum