let k be Element of NAT ; :: thesis: for X being non empty set st 0 < k & k + 1 c= card X holds
for A being finite Subset of X st card A = k - 1 holds
meet (^^ A,X,k) = A
let X be non empty set ; :: thesis: ( 0 < k & k + 1 c= card X implies for A being finite Subset of X st card A = k - 1 holds
meet (^^ A,X,k) = A )
assume A1: ( 0 < k & k + 1 c= card X ) ; :: thesis: for A being finite Subset of X st card A = k - 1 holds
meet (^^ A,X,k) = A
let A be finite Subset of X; :: thesis: ( card A = k - 1 implies meet (^^ A,X,k) = A )
assume A2: card A = k - 1 ; :: thesis: meet (^^ A,X,k) = A
^^ A,X,k = ^^ A,X by A1, A2, Def13;
hence meet (^^ A,X,k) = A by A1, A2, Th26; :: thesis: verum