set M = ModelSP (Inf_seq S);
deffunc H₁( object ) -> Element of ModelSP (Inf_seq S) = Not_0 ($1,S);
ex o being UnOp of (ModelSP (Inf_seq S)) st
for f being object st f in ModelSP (Inf_seq S) holds
o . f = H₁(f) from MODELC_1:sch 4();
hence ex b₁ being UnOp of (ModelSP (Inf_seq S)) st
for f being object st f in ModelSP (Inf_seq S) holds
b₁ . f = Not_0 (f,S) ; :: thesis: verum