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