let A be QC-alphabet ; for H being Element of QC-WFF A
for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let H be Element of QC-WFF A; for x being bound_QC-variable of A holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
let x be bound_QC-variable of A; Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))}
thus
Subformulae (All (x,H)) c= (Subformulae H) \/ {(All (x,H))}
XBOOLE_0:def 10 (Subformulae H) \/ {(All (x,H))} c= Subformulae (All (x,H))
let a be object ; TARSKI:def 3 ( not a in (Subformulae H) \/ {(All (x,H))} or a in Subformulae (All (x,H)) )
assume A3:
a in (Subformulae H) \/ {(All (x,H))}
; a in Subformulae (All (x,H))
hence
a in Subformulae (All (x,H))
by A3, A4, XBOOLE_0:def 3; verum