let k be Element of NAT ; :: thesis: for X being non empty set st 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: ( 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: 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

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