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