let O1, O2 be ExtReal; :: thesis: ( ( 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 ) )

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: verum

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 ) )

now :: thesis: ( 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 G1 being Subset-Family of X st

( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

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 G1 being Subset-Family of X st

( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

assume
Fx is finite-order
; :: thesis: ( ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G1 being Subset-Family of X st

( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

assume A14: for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ; :: thesis: ( ex G1 being Subset-Family of X st

( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

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: ( ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

assume A18: for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ; :: thesis: ( ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

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: O1 = O2

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: verum

end;meet Gx is empty ) & ex G1 being Subset-Family of X st

( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

assume A14: for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ; :: thesis: ( ex G1 being Subset-Family of X st

( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

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: ( ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

assume A18: for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ; :: thesis: ( ex G2 being Subset-Family of X st

( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 )

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: O1 = O2

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: verum

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: verum