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):]

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

proof

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
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;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