set Y = ModelSP (Inf_seq AtomicFamily );
set z = AtomicAsgn {} ;
set M = { x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } ;
A1: { 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 ex y being Element of ModelSP (Inf_seq AtomicFamily ) st
( x = y & ex a being set st y = AtomicAsgn a ) ;
hence x in ModelSP (Inf_seq AtomicFamily ) ; :: thesis: verum

end;

AtomicAsgn {} in { x where x is Element of ModelSP (Inf_seq AtomicFamily ) : ex a being set st x = AtomicAsgn a } ;
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