let A be QC-alphabet ; :: thesis: for t, u being QC-symbol of A
for p, q being Element of CQC-WFF A
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) holds
u < t
let t, u be QC-symbol of A; :: thesis: for p, q being Element of CQC-WFF A
for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) holds
u < t
let p, q be Element of CQC-WFF A; :: thesis: for f being Element of Funcs ((bound_QC-variables A),(bound_QC-variables A))
for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) holds
u < t
let f be Element of Funcs ((bound_QC-variables A),(bound_QC-variables A)); :: thesis: for K being Element of Fin (bound_QC-variables A) st [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) holds
u < t
let K be Element of Fin (bound_QC-variables A); :: thesis: ( [q,t,K,f] in SepQuadruples p & x. u in f .: (still_not-bound_in q) implies u < t )
assume that
A1: [q,t,K,f] in SepQuadruples p and
A2: x. u in f .: (still_not-bound_in q) ; :: thesis: u < t
f .: (still_not-bound_in q) c= f .: ((still_not-bound_in p) \/ K) by A1, Th38, RELAT_1:123;
then x. u in f .: ((still_not-bound_in p) \/ K) by A2;
then x. u in (f .: (still_not-bound_in p)) \/ (f .: K) by RELAT_1:120;
then ( x. u in f .: (still_not-bound_in p) or x. u in f .: K ) by XBOOLE_0:def 3;
hence u < t by A1, Th39, Th41; :: thesis: verum