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:156;
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:153;
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