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