deffunc H₁( set , Function of S,BOOLEAN , Function of S,BOOLEAN ) -> Element of BOOLEAN = EUntill_univ $1,$2,$3,R;
consider IT being set such that
A1: IT in ModelSP S and
A2: for s being set st s in S holds
( H₁(s, Fid f,S, Fid g,S) = TRUE iff (Fid IT,S) . s = TRUE ) from MODELC_1:sch 6();
take IT ; :: thesis: ( IT is Element of ModelSP S & ( for s being set st s in S holds
( EUntill_univ s,(Fid f,S),(Fid g,S),R = TRUE iff (Fid IT,S) . s = TRUE ) ) )
thus ( IT is Element of ModelSP S & ( for s being set st s in S holds
( EUntill_univ s,(Fid f,S),(Fid g,S),R = TRUE iff (Fid IT,S) . s = TRUE ) ) ) by A1, A2; :: thesis: verum