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