theorem Th27: :: GOEDELCP:27

for Al being QC-alphabet
for X, Y being Subset of (CQC-WFF Al) holds still_not-bound_in (X \/ Y) = (still_not-bound_in X) \/ (still_not-bound_in Y)