let t be quasi-type of C; :: thesis: ex f being valuation of C st
( (adjs t) at f c= adjs t & (the_base_of t) at f = the_base_of t )
take f = the empty valuation of C; :: thesis: ( (adjs t) at f c= adjs t & (the_base_of t) at f = the_base_of t )
thus (adjs t) at f c= adjs t :: thesis: (the_base_of t) at f = the_base_of t

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (adjs t) at f or x in adjs t )
assume x in (adjs t) at f ; :: thesis: x in adjs t
then ex a being quasi-adjective of C st
( x = a at f & a in adjs t ) ;
hence x in adjs t by ABCMIZ_1:139; :: thesis: verum

end;

thus (the_base_of t) at f = the_base_of t by ABCMIZ_1:139; :: thesis: verum