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