let q, p be Element of CQC-WFF ; :: thesis: for m, i being Element of NAT
for f being Element of Funcs (bound_QC-variables,bound_QC-variables)
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in q) holds
i < m
let m, i be Element of NAT ; :: thesis: for f being Element of Funcs (bound_QC-variables,bound_QC-variables)
for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in q) holds
i < m
let f be Element of Funcs (bound_QC-variables,bound_QC-variables); :: thesis: for K being Finite_Subset of bound_QC-variables st [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in q) holds
i < m
let K be Finite_Subset of bound_QC-variables; :: thesis: ( [q,m,K,f] in SepQuadruples p & x. i in f .: (still_not-bound_in q) implies i < m )
assume that
A1: [q,m,K,f] in SepQuadruples p and
A2: x. i in f .: (still_not-bound_in q) ; :: thesis: i < m
f .: (still_not-bound_in q) c= f .: ((still_not-bound_in p) \/ K) by A1, Th39, RELAT_1:123;
then x. i in f .: ((still_not-bound_in p) \/ K) by A2;
then x. i in (f .: (still_not-bound_in p)) \/ (f .: K) by RELAT_1:120;
then ( x. i in f .: (still_not-bound_in p) or x. i in f .: K ) by XBOOLE_0:def 3;
hence i < m by A1, Th40, Th42; :: thesis: verum