deffunc H₁( set , Function of S,BOOLEAN , Function of S,BOOLEAN ) -> Element of BOOLEAN = EUntill_univ $1,$2,$3,R;
for h1, h2 being set st h1 in ModelSP S & ( for s being set st s in S holds
( H₁(s, Fid f,S, Fid g,S) = TRUE iff (Fid h1,S) . s = TRUE ) ) & h2 in ModelSP S & ( for s being set st s in S holds
( H₁(s, Fid f,S, Fid g,S) = TRUE iff (Fid h2,S) . s = TRUE ) ) holds
h1 = h2 from MODELC_1:sch 7();
hence for b₁, b₂ being Element of ModelSP S st ( for s being set st s in S holds
( EUntill_univ s,(Fid f,S),(Fid g,S),R = TRUE iff (Fid b₁,S) . s = TRUE ) ) & ( for s being set st s in S holds
( EUntill_univ s,(Fid f,S),(Fid g,S),R = TRUE iff (Fid b₂,S) . s = TRUE ) ) holds
b₁ = b₂ ; :: thesis: verum