let X be infinite set ; :: thesis: for A being Subset of X st A is finite holds
A ` is infinite
let A be Subset of X; :: thesis: ( A is finite implies A ` is infinite )
A \/ (A `) = [#] X by SUBSET_1:10
.= X ;
hence ( A is finite implies A ` is infinite ) ; :: thesis: verum