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

A1: X |- (All (x,p)) => p by CQC_THE1:93;
assume X |- All (x,p) ; :: thesis: X |- p
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