let A, B be set ; :: thesis: ( A is_finer_than B implies A \/ B is_finer_than B )
assume A is_finer_than B ; :: thesis: A \/ B is_finer_than B
then A \/ B is_finer_than B \/ B by Th61;
hence A \/ B is_finer_than B ; :: thesis: verum