let C be initialized ConstructorSignature; :: thesis: for f being valuation of C
for A being Subset of (QuasiAdjs C)
for a being quasi-adjective of C st A = {a} holds
A at f = {(a at f)}
let f be valuation of C; :: thesis: for A being Subset of (QuasiAdjs C)
for a being quasi-adjective of C st A = {a} holds
A at f = {(a at f)}
let A be Subset of (QuasiAdjs C); :: thesis: for a being quasi-adjective of C st A = {a} holds
A at f = {(a at f)}
let a be quasi-adjective of C; :: thesis: ( A = {a} implies A at f = {(a at f)} )
assume A1: A = {a} ; :: thesis: A at f = {(a at f)}
thus A at f c= {(a at f)} :: according to XBOOLE_0:def 10 :: thesis: {(a at f)} c= A at f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A at f or x in {(a at f)} )
assume x in A at f ; :: thesis: x in {(a at f)}
then ex b being quasi-adjective of C st
( x = b at f & b in A ) ;
then x = a at f by A1, TARSKI:def 1;
hence x in {(a at f)} by TARSKI:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(a at f)} or x in A at f )
assume x in {(a at f)} ; :: thesis: x in A at f
then A2: x = a at f by TARSKI:def 1;
a in A by A1, TARSKI:def 1;
hence x in A at f by A2; :: thesis: verum