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