thus ( x. 0 in Free H implies { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ) :: thesis: ( not x. 0 in Free H implies {} is Subset of M )

proof

set X = { m where m is Element of M : M,v / ((x. 0),m) |= H } ;
assume x. 0 in Free H ; :: thesis: { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M
{ m where m is Element of M : M,v / ((x. 0),m) |= H } c= M

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in { m where m is Element of M : M,v / ((x. 0),m) |= H } or u in M )
assume u in { m where m is Element of M : M,v / ((x. 0),m) |= H } ; :: thesis: u in M
then ex m being Element of M st
( u = m & M,v / ((x. 0),m) |= H ) ;
hence u in M ; :: thesis: verum

end;

hence { m where m is Element of M : M,v / ((x. 0),m) |= H } is Subset of M ; :: thesis: verum

end;

thus ( not x. 0 in Free H implies {} is Subset of M ) by XBOOLE_1:2; :: thesis: verum