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

now

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

end;

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