defpred S₁[ set ] means ex g being PartFunc of X,Y st
( g = $1 & g is total & f tolerates g );
let F1, F2 be set ; :: thesis: ( ( for x being set holds
( x in F1 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) & ( for x being set holds
( x in F2 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) implies F1 = F2 )
assume that
A5: for x being set holds
( x in F1 iff S₁[x] ) and
A6: for x being set holds
( x in F2 iff S₁[x] ) ; :: thesis: F1 = F2
thus F1 = F2 from XBOOLE_0:sch 2(A5, A6); :: thesis: verum