deffunc H1( set , Function of (Inf_seq S),BOOLEAN, Function of (Inf_seq S),BOOLEAN) -> object = (Castboolean ($2 . $1)) '&' (Castboolean ($3 . $1));
consider IT being set such that
A1:
( IT in ModelSP (Inf_seq S) & ( for t being set st t in Inf_seq S holds
( H1(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
; ( 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; verum