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