set Q = { t where t is Element of P * : ( t in P & A . t <> 0 ) } ;
{ t where t is Element of P * : ( t in P & A . t <> 0 ) } c= P

proof

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

end;

hence { t where t is Element of P * : ( t in P & A . t <> 0 ) } is Subset of P ; :: thesis: verum