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