defpred S₁[ object ] means ex F being Element of QC-WFF A st
( F = $1 & F is_subformula_of H );
let X, Y be set ; :: 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 ) ) ) & ( for a being object holds
( a in Y iff ex F being Element of QC-WFF A st
( F = a & F is_subformula_of H ) ) ) implies X = Y )
assume that
A3: for a being object holds
( a in X iff S₁[a] ) and
A4: for a being object holds
( a in Y iff S₁[a] ) ; :: thesis: X = Y
thus X = Y from XBOOLE_0:sch 2(A3, A4); :: thesis: verum