let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A
for X being Subset of (CQC-WFF A)
for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
let p be Element of CQC-WFF A; :: thesis: for X being Subset of (CQC-WFF A)
for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
let X be Subset of (CQC-WFF A); :: thesis: for x being bound_QC-variable of A holds
( X |- All (x,p) iff X |- p )
let x be bound_QC-variable of A; :: 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:56;
assume X |- All (x,p) ; :: thesis: X |- p
hence X |- p by A1, CQC_THE1:55; :: thesis: verum
end;
thus ( X |- p implies X |- All (x,p) ) by CQC_THE2:90; :: thesis: verum