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 )
card (n + 1) = card (card (n + 1)) ;
then A1: card (n + 1) = n + 1 by CARD_1:71;
card (n + 2) = card (card (n + 2)) ;
then A2: card (n + 2) = n + 2 by CARD_1:71;
assume A3: 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 A3, XREAL_1:8;
then (order f) + 1 < (n + 1) + 1 by NAT_1:13;
then A4: (order f) + 1 in n + 2 by NAT_1:45;
let Gx be Subset-Family of X; :: thesis: ( Gx c= Fx & n + 1 in card Gx implies meet Gx is empty )
assume that
A5: Gx c= Fx and
A6: n + 1 in card Gx ; :: thesis: meet Gx is empty
nextcard (n + 1) c= card Gx by A6, CARD_3:107;
then card ((n + 1) + 1) c= card Gx by A1, NAT_1:43;
hence meet Gx is empty by A5, A2, A4, Def2; :: thesis: verum