deffunc H₁( set , Function of S,BOOLEAN) -> Element of BOOLEAN = EneXt_univ ($1,$2,R);
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
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b₁,S)) . s = TRUE ) ) & ( for s being set st s in S holds
( EneXt_univ (s,(Fid (f,S)),R) = TRUE iff (Fid (b₂,S)) . s = TRUE ) ) holds
b₁ = b₂ ; :: thesis: verum