defpred S₁[ set ] means ex v being Element of Valuations_in A st
( $1 = v & v *' ll in r );
deffunc H₁( set ) -> Element of BOOLEAN = TRUE ;
deffunc H₂( set ) -> Element of BOOLEAN = FALSE ;
A1: for x being set st x in Valuations_in A holds
( ( S₁[x] implies H₁(x) in BOOLEAN ) & ( not S₁[x] implies H₂(x) in BOOLEAN ) ) ;
consider f being Function of (Valuations_in A),BOOLEAN such that
A2: for x being set st x in Valuations_in A holds
( ( S₁[x] implies f . x = H₁(x) ) & ( not S₁[x] implies f . x = H₂(x) ) ) from FUNCT_2:sch 5(A1);
( dom f = Valuations_in A & rng f c= BOOLEAN ) by FUNCT_2:def 1, RELAT_1:def 19;
then reconsider f = f as Element of Funcs ((Valuations_in A),BOOLEAN) by FUNCT_2:def 2;
take f ; :: thesis: for v being Element of Valuations_in A holds
( ( v *' ll in r implies f . v = TRUE ) & ( not v *' ll in r implies f . v = FALSE ) )
let v be Element of Valuations_in A; :: thesis: ( ( v *' ll in r implies f . v = TRUE ) & ( not v *' ll in r implies f . v = FALSE ) )
( ( for v9 being Element of Valuations_in A holds
( not v = v9 or not v9 *' ll in r ) ) implies f . v = FALSE ) by A2;
hence ( ( v *' ll in r implies f . v = TRUE ) & ( not v *' ll in r implies f . v = FALSE ) ) by A2; :: thesis: verum