set P = { t where t is Element of T : A . t <> 0 } ;
{ t where t is Element of T : A . t <> 0 } c= T

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { t where t is Element of T : A . t <> 0 } or a in T )
assume a in { t where t is Element of T : A . t <> 0 } ; :: thesis: a in T
then consider t being Element of T such that
A1: a = t and
A . t <> 0 ;
thus a in T by A1; :: thesis: verum

end;

hence { t where t is Element of T : A . t <> 0 } is Subset of T ; :: thesis: verum