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;
card n = card (card n) ;
then A5: card n = n by CARD_1:40;
then not card n in card G by A1, A3, A4;
then card G c= n by A5, 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