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

A1: now :: thesis: ( ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) implies (FOR_ALL (x,p)) . v = FALSE )

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

end;

now :: thesis: ( (FOR_ALL (x,p)) . v = FALSE implies ex v1 being Element of Valuations_in (Al,A) st
( p . v1 = FALSE & ( for y being bound_QC-variable of Al st x <> y holds
v1 . y = v . y ) ) )

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