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