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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) } or x in bound_QC-variables )
assume x in { (l1 . k) where k is Element of NAT : ( 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) } ; :: thesis: x in bound_QC-variables
then ex k being Element of NAT st
( l1 . k = x & 1 <= k & k <= len l1 & l1 . k in bound_QC-variables ) ;
hence x in bound_QC-variables ; :: thesis: verum

end;

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