let s, h be QC-formula; :: thesis: for y being bound_QC-variable holds
( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
let y be bound_QC-variable; :: thesis: ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) )
still_not-bound_in (s => h) = (still_not-bound_in s) \/ (still_not-bound_in h) by QC_LANG3:20;
hence ( y in still_not-bound_in (s => h) iff ( y in still_not-bound_in s or y in still_not-bound_in h ) ) by XBOOLE_0:def 3; :: thesis: verum