let x be bound_QC-variable; :: thesis: for S being Element of CQC-Sub-WFF st x in dom (@ (S `2)) holds
(@ (S `2)) . x is bound_QC-variable
let S be Element of CQC-Sub-WFF ; :: thesis: ( x in dom (@ (S `2)) implies (@ (S `2)) . x is bound_QC-variable )
assume x in dom (@ (S `2)) ; :: thesis: (@ (S `2)) . x is bound_QC-variable
then (@ (S `2)) . x in rng (@ (S `2)) by FUNCT_1:3;
hence (@ (S `2)) . x is bound_QC-variable ; :: thesis: verum