defpred S₁[ object ] means ex F being Element of QC-WFF A st
( F = $1 & F is_subformula_of H );
consider X being set such that
A1: for a being object holds
( a in X iff ( a in QC-WFF A & S₁[a] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for a being object holds
( a in X iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) )
let a be object ; :: thesis: ( a in X iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) )
thus ( a in X implies ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) by A1; :: thesis: ( ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) implies a in X )
given F being Element of QC-WFF A such that A2: ( F = a & F is_subformula_of H ) ; :: thesis: a in X
thus a in X by A1, A2; :: thesis: verum