let k be Element of NAT ; 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
^^ (A,X,k) is STAR
let X be non empty set ; ( k + 1 c= card X implies for A being finite Subset of X st card A = k - 1 holds
^^ (A,X,k) is STAR )
assume A1:
k + 1 c= card X
; for A being finite Subset of X st card A = k - 1 holds
^^ (A,X,k) is STAR
let A be finite Subset of X; ( card A = k - 1 implies ^^ (A,X,k) is STAR )
assume A2:
card A = k - 1
; ^^ (A,X,k) is STAR
^^ (A,X,k) = ^^ (A,X)
by A1, A2, Def13;
hence
^^ (A,X,k) is STAR
by A2; verum