deffunc H1( set , Function of S,BOOLEAN) -> object = 'not' (Castboolean ($2 . $1));
for g1, g2 being set st g1 in ModelSP S & ( for s being set st s in S holds
( H1(s, Fid (f,S)) = TRUE iff (Fid (g1,S)) . s = TRUE ) ) & g2 in ModelSP S & ( for s being set st s in S holds
( H1(s, Fid (f,S)) = TRUE iff (Fid (g2,S)) . s = TRUE ) ) holds
g1 = g2
from MODELC_1:sch 3();
hence
for b1, b2 being Element of ModelSP S st ( for s being set st s in S holds
( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b1,S)) . s = TRUE ) ) & ( for s being set st s in S holds
( 'not' (Castboolean ((Fid (f,S)) . s)) = TRUE iff (Fid (b2,S)) . s = TRUE ) ) holds
b1 = b2
; verum