deffunc H₁( set , Function of (Inf_seq S),BOOLEAN, Function of (Inf_seq S),BOOLEAN) -> Element of BOOLEAN = Until_univ ($1,$2,$3,S);
consider IT being set such that
A1: ( IT 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 (IT,(Inf_seq S))) . t = TRUE ) ) ) from MODELC_1:sch 6();
take IT ; :: thesis: ( IT is Element of ModelSP (Inf_seq S) & ( for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (IT,(Inf_seq S))) . t = TRUE ) ) )
thus ( IT is Element of ModelSP (Inf_seq S) & ( for t being set st t in Inf_seq S holds
( Until_univ (t,(Fid (f,(Inf_seq S))),(Fid (g,(Inf_seq S))),S) = TRUE iff (Fid (IT,(Inf_seq S))) . t = TRUE ) ) ) by A1; :: thesis: verum