set IT = { (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } ;

now :: thesis: for x being object st x in { (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } holds
x in bound_QC-variables A

let x be object ; :: thesis: ( x in { (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } implies x in bound_QC-variables A )
assume x in { (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } ; :: thesis: x in bound_QC-variables A
then ex k being Nat st
( x = ll . k & 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) ;
hence x in bound_QC-variables A ; :: thesis: verum

end;

hence { (ll . k) where k is Nat : ( 1 <= k & k <= len ll & ll . k in bound_QC-variables A ) } is Subset of (bound_QC-variables A) by TARSKI:def 3; :: thesis: verum