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