set D = { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ;
{ a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } c= [:(Fin X),(Fin X):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } or x in [:(Fin X),(Fin X):] )
assume x in { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } ; :: thesis: x in [:(Fin X),(Fin X):]
then ex a being Element of [:(Fin X),(Fin X):] st
( x = a & a `1 misses a `2 ) ;
hence x in [:(Fin X),(Fin X):] ; :: thesis: verum

end;

hence { a where a is Element of [:(Fin X),(Fin X):] : a `1 misses a `2 } is Subset of [:(Fin X),(Fin X):] ; :: thesis: verum