let O1, O2 be ExtReal; :: thesis:

assume Fx is finite-order ; :: thesis:
assume A14: for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ; :: thesis:
given G1 being Subset-Family of X such that A15: G1 c= Fx and
A16: card G1 = O1 + 1 and
A17: ( not meet G1 is empty or G1 is empty ) ; :: thesis:
assume A18: for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ; :: thesis:
given G2 being Subset-Family of X such that A19: G2 c= Fx and
A20: card G2 = O2 + 1 and
A21: ( not meet G2 is empty or G2 is empty ) ; :: thesis:
not card G2 in card G1 by A15, A17, A18, A20;
then A22: card G1 c= card G2 by CARD_1:3;
not card G1 in card G2 by A14, A16, A19, A21;
then card G1 = card G2 by A22, CARD_1:3;
hence O1 = O2 by A16, A20, XXREAL_3:11; :: thesis:

end;

hence ( ( Fx is finite-order & ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds
meet Gx is empty ) & ex Gx being Subset-Family of X st
( Gx c= Fx & card Gx = O2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies O1 = O2 ) & ( not Fx is finite-order & O1 = +infty & O2 = +infty implies O1 = O2 ) ) ; :: thesis: