defpred S₁[ object ] 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 object holds
( x in F1 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ) & ( for x being object 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
A3: for x being object holds
( x in F1 iff S₁[x] ) and
A4: for x being object holds
( x in F2 iff S₁[x] ) ; :: thesis: F1 = F2
thus F1 = F2 from XBOOLE_0:sch 2(A3, A4); :: thesis: verum