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