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