let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being QC-formula of A holds
( All (x,p) is closed iff still_not-bound_in p c= {x} )
let x be bound_QC-variable of A; :: thesis: for p being QC-formula of A holds
( All (x,p) is closed iff still_not-bound_in p c= {x} )
let p be QC-formula of A; :: thesis: ( All (x,p) is closed iff still_not-bound_in p c= {x} )
thus ( All (x,p) is closed implies still_not-bound_in p c= {x} ) :: thesis: ( still_not-bound_in p c= {x} implies All (x,p) is closed )
proof
assume still_not-bound_in (All (x,p)) = {} ; :: according to QC_LANG1:def 31 :: thesis: still_not-bound_in p c= {x}
then {} = (still_not-bound_in p) \ {x} by Th12;
hence still_not-bound_in p c= {x} by XBOOLE_1:37; :: thesis: verum
end;
assume still_not-bound_in p c= {x} ; :: thesis: All (x,p) is closed
then {} = (still_not-bound_in p) \ {x} by XBOOLE_1:37;
hence still_not-bound_in (All (x,p)) = {} by Th12; :: according to QC_LANG1:def 31 :: thesis: verum