let n be Nat; :: thesis: for X being set

for Fx being Subset-Family of X st order Fx <= n holds

for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty

let X be set ; :: thesis: for Fx being Subset-Family of X st order Fx <= n holds

for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty

let Fx be Subset-Family of X; :: thesis: ( order Fx <= n implies for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty )

A1: card (n + 1) = n + 1 ;

assume A2: order Fx <= n ; :: thesis: for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty

then reconsider f = Fx as finite-order Subset-Family of X by Th1;

(order f) + 1 <= n + 1 by A2, XREAL_1:6;

then (order f) + 1 < (n + 1) + 1 by NAT_1:13;

then A3: (order f) + 1 in Segm (n + 2) by NAT_1:44;

let Gx be Subset-Family of X; :: thesis: ( Gx c= Fx & n + 1 in card Gx implies meet Gx is empty )

assume that

A4: Gx c= Fx and

A5: n + 1 in card Gx ; :: thesis: meet Gx is empty

nextcard (Segm (n + 1)) c= card Gx by A5, CARD_3:90;

then card (Segm ((n + 1) + 1)) c= card Gx by A1, NAT_1:42;

hence meet Gx is empty by A4, A3, Def2; :: thesis: verum

for Fx being Subset-Family of X st order Fx <= n holds

for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty

let X be set ; :: thesis: for Fx being Subset-Family of X st order Fx <= n holds

for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty

let Fx be Subset-Family of X; :: thesis: ( order Fx <= n implies for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty )

A1: card (n + 1) = n + 1 ;

assume A2: order Fx <= n ; :: thesis: for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty

then reconsider f = Fx as finite-order Subset-Family of X by Th1;

(order f) + 1 <= n + 1 by A2, XREAL_1:6;

then (order f) + 1 < (n + 1) + 1 by NAT_1:13;

then A3: (order f) + 1 in Segm (n + 2) by NAT_1:44;

let Gx be Subset-Family of X; :: thesis: ( Gx c= Fx & n + 1 in card Gx implies meet Gx is empty )

assume that

A4: Gx c= Fx and

A5: n + 1 in card Gx ; :: thesis: meet Gx is empty

nextcard (Segm (n + 1)) c= card Gx by A5, CARD_3:90;

then card (Segm ((n + 1) + 1)) c= card Gx by A1, NAT_1:42;

hence meet Gx is empty by A4, A3, Def2; :: thesis: verum