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

proof

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

end;

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