let a be Element of F; :: thesis: a is Subset of X
thus a is Subset of X by FINSUB_1:16; :: thesis: verum