let W be set ; :: thesis: ( W is Tarski implies Rank (card W) is Tarski )
assume A1: W is Tarski ; :: thesis: Rank (card W) is Tarski
set B = Rank (card W);
thus for X, Y being set st X in Rank (card W) & Y c= X holds
Y in Rank (card W) by CLASSES1:41; :: according to CLASSES1:def 1,CLASSES1:def 2 :: thesis: ( ( for b1 being set holds
( not b1 in Rank (card W) or bool b1 in Rank (card W) ) ) & ( for b1 being set holds
( not b1 c= Rank (card W) or b1, Rank (card W) are_equipotent or b1 in Rank (card W) ) ) )
now :: thesis: ( W <> {} implies for X being set st X in Rank (card W) holds
bool X in Rank (card W) )
A2: card W is limit_ordinal by A1, Th19;
assume A3: W <> {} ; :: thesis: for X being set st X in Rank (card W) holds
bool X in Rank (card W)
thus for X being set st X in Rank (card W) holds
bool X in Rank (card W) :: thesis: verum
proof
let X be set ; :: thesis: ( X in Rank (card W) implies bool X in Rank (card W) )
assume X in Rank (card W) ; :: thesis: bool X in Rank (card W)
then consider A being Ordinal such that
A4: A in card W and
A5: X in Rank A by A3, A2, CLASSES1:31;
A6: bool X in Rank (succ A) by A5, CLASSES1:42;
succ A in card W by A2, A4, ORDINAL1:28;
hence bool X in Rank (card W) by A2, A6, CLASSES1:31; :: thesis: verum
end;
end;
hence ( ( for b1 being set holds
( not b1 in Rank (card W) or bool b1 in Rank (card W) ) ) & ( for b1 being set holds
( not b1 c= Rank (card W) or b1, Rank (card W) are_equipotent or b1 in Rank (card W) ) ) ) by A1, Th36, CLASSES1:29; :: thesis: verum