let A be non empty set ; :: thesis: for x being bound_QC-variable
for v being Element of Valuations_in A
for p being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) )
let x be bound_QC-variable; :: thesis: for v being Element of Valuations_in A
for p being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) )
let v be Element of Valuations_in A; :: thesis: for p being Element of Funcs ((Valuations_in A),BOOLEAN) holds
( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) )
let p be Element of Funcs ((Valuations_in A),BOOLEAN); :: thesis: ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) )

A1: now

assume ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) ; :: thesis: (FOR_ALL (x,p)) . v = FALSE
then FALSE in { (p . v99) where v99 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v99 . y = v . y } ;
then ALL { (p . v99) where v99 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v99 . y = v . y } = FALSE by MARGREL1:17;
hence (FOR_ALL (x,p)) . v = FALSE by Def7; :: thesis: verum

end;

now

assume (FOR_ALL (x,p)) . v = FALSE ; :: thesis: ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) )
then ALL { (p . v99) where v99 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v99 . y = v . y } = FALSE by Def7;
then FALSE in { (p . v99) where v99 is Element of Valuations_in A : for y being bound_QC-variable st x <> y holds
v99 . y = v . y } by MARGREL1:17;
hence ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) ; :: thesis: verum

end;

hence ( (FOR_ALL (x,p)) . v = FALSE iff ex v1 being Element of Valuations_in A st
( p . v1 = FALSE & ( for y being bound_QC-variable st x <> y holds
v1 . y = v . y ) ) ) by A1; :: thesis: verum