set M = { x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } ;
set z = AtomicAsgn {} ;
set Y = ModelSP (Inf_seq AtomicFamily );
A1: AtomicAsgn {} in { x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } ;
{ x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } c= ModelSP (Inf_seq AtomicFamily )

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } or x in ModelSP (Inf_seq AtomicFamily ) )
assume x in { x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } ; :: thesis: x in ModelSP (Inf_seq AtomicFamily )
then consider y being Element of ModelSP (Inf_seq AtomicFamily ) such that
B1: x = y and
ex a being set st y = AtomicAsgn a ;
thus x in ModelSP (Inf_seq AtomicFamily ) by B1; :: thesis: verum

end;

hence { x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } is non empty Subset of (ModelSP (Inf_seq AtomicFamily )) by A1; :: thesis: verum