let n be Nat; :: thesis: for D being non empty set
for D1 being non empty Subset of D holds n -tuples_on D1 c= n -tuples_on D
let D be non empty set ; :: thesis: for D1 being non empty Subset of D holds n -tuples_on D1 c= n -tuples_on D
let D1 be non empty Subset of D; :: thesis: n -tuples_on D1 c= n -tuples_on D
(n -tuples_on D) /\ (n -tuples_on D1) = n -tuples_on D1 by MARGREL1:21;
hence n -tuples_on D1 c= n -tuples_on D by XBOOLE_1:17; :: thesis: verum