let X be non empty set ; :: thesis: for B being Element of Fin X st B <> {} holds
ex x being Element of X st x in B
let B be Element of Fin X; :: thesis: ( B <> {} implies ex x being Element of X st x in B )
set x = the Element of B;
assume A1: B <> {} ; :: thesis: ex x being Element of X st x in B
then reconsider x = the Element of B as Element of X by Th6;
take x ; :: thesis: x in B
thus x in B by A1; :: thesis: verum