consider G being Subset-Family of X such that

A1: G c= F and

A2: card G = (order F) + 1 and

A3: ( not meet G is empty or G is empty ) by Def2;

consider n being Nat such that

A4: for H being Subset-Family of X st H c= F & n in card H holds

meet H is empty by Def1;

not card n in card G by A1, A3, A4;

then card G c= n by CARD_1:4;

then reconsider G = G as finite Subset-Family of X ;

(order F) + 1 = ((card G) - 1) + 1 by A2;

hence (order F) + 1 is natural ; :: thesis: verum

A1: G c= F and

A2: card G = (order F) + 1 and

A3: ( not meet G is empty or G is empty ) by Def2;

consider n being Nat such that

A4: for H being Subset-Family of X st H c= F & n in card H holds

meet H is empty by Def1;

not card n in card G by A1, A3, A4;

then card G c= n by CARD_1:4;

then reconsider G = G as finite Subset-Family of X ;

(order F) + 1 = ((card G) - 1) + 1 by A2;

hence (order F) + 1 is natural ; :: thesis: verum