let X be non empty set ; :: thesis: for B being Element of Fin X
for x being set st x in B holds
x is Element of X
let B be Element of Fin X; :: thesis: for x being set st x in B holds
x is Element of X
let x be set ; :: thesis: ( x in B implies x is Element of X )
assume A1: x in B ; :: thesis: x is Element of X
B c= X by FINSUB_1:def 5;
hence x is Element of X by A1; :: thesis: verum