let C be initialized ConstructorSignature; :: thesis: for A being Subset of (QuasiAdjs C)
for f1, f2 being valuation of C holds (A at f1) at f2 = A at (f1 at f2)
let A be Subset of (QuasiAdjs C); :: thesis: for f1, f2 being valuation of C holds (A at f1) at f2 = A at (f1 at f2)
let f1, f2 be valuation of C; :: thesis: (A at f1) at f2 = A at (f1 at f2)
thus (A at f1) at f2 c= A at (f1 at f2) :: according to XBOOLE_0:def 10 :: thesis: A at (f1 at f2) c= (A at f1) at f2
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A at f1) at f2 or x in A at (f1 at f2) )
assume x in (A at f1) at f2 ; :: thesis: x in A at (f1 at f2)
then consider a being quasi-adjective of C such that
A1: x = a at f2 and
A2: a in A at f1 ;
consider b being quasi-adjective of C such that
A3: a = b at f1 and
A4: b in A by A2;
x = b at (f1 at f2) by A1, A3, Th149;
hence x in A at (f1 at f2) by A4; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A at (f1 at f2) or x in (A at f1) at f2 )
assume x in A at (f1 at f2) ; :: thesis: x in (A at f1) at f2
then consider a being quasi-adjective of C such that
A5: x = a at (f1 at f2) and
A6: a in A ;
A7: x = (a at f1) at f2 by A5, Th149;
a at f1 in A at f1 by A6;
hence x in (A at f1) at f2 by A7; :: thesis: verum