let p be Element of CQC-WFF ; :: thesis: for X being Subset of CQC-WFF
for x being bound_QC-variable holds
( X |- All x,p iff X |- p )
let X be Subset of CQC-WFF ; :: thesis: for x being bound_QC-variable holds
( X |- All x,p iff X |- p )
let x be bound_QC-variable; :: thesis: ( X |- All x,p iff X |- p )
thus ( X |- All x,p implies X |- p ) :: thesis: ( X |- p implies X |- All x,p )

proof

assume A1: X |- All x,p ; :: thesis: X |- p
X |- (All x,p) => p by CQC_THE1:93;
hence X |- p by A1, CQC_THE1:92; :: thesis: verum

end;

thus ( X |- p implies X |- All x,p ) by CQC_THE2:94; :: thesis: verum