deffunc H₁( set , Function of S,BOOLEAN, Function of S,BOOLEAN) -> object = (Castboolean ($2 . $1)) '&' (Castboolean ($3 . $1));
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
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (IT,S)) . s = TRUE ) ) )
thus ( IT is Element of ModelSP S & ( for s being set st s in S holds
( (Castboolean ((Fid (f,S)) . s)) '&' (Castboolean ((Fid (g,S)) . s)) = TRUE iff (Fid (IT,S)) . s = TRUE ) ) ) by A1, A2; :: thesis: verum