deffunc H₁( set , Function of (Inf_seq S),BOOLEAN , Function of (Inf_seq S),BOOLEAN ) -> set = (Castboolean ($2 . $1)) '&' (Castboolean ($3 . $1));
consider IT being set such that
A1: IT in ModelSP (Inf_seq S) and
A2: 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
( (Castboolean ((Fid f,(Inf_seq S)) . t)) '&' (Castboolean ((Fid g,(Inf_seq S)) . t)) = 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
( (Castboolean ((Fid f,(Inf_seq S)) . t)) '&' (Castboolean ((Fid g,(Inf_seq S)) . t)) = TRUE iff (Fid IT,(Inf_seq S)) . t = TRUE ) ) ) by A1, A2; :: thesis: verum