let A, B be set ; :: thesis: ( B is c=directed & A is_finer_than B implies A \/ B is c=directed )
assume A1: ( B is c=directed & A is_finer_than B ) ; :: thesis: A \/ B is c=directed
reconsider BB = B as c=directed set by A1;
reconsider X = A \/ BB as non empty set ;
now :: thesis: for a, b being set st a in X & b in X holds
ex cc being set st
( a \/ b c= cc & cc in X )
let a, b be set ; :: thesis: ( a in X & b in X implies ex cc being set st
( a \/ b c= cc & cc in X ) )
assume a in X ; :: thesis: ( b in X implies ex cc being set st
( a \/ b c= cc & cc in X ) )
then consider aa being set such that
A2: ( aa in B & a c= aa ) by SETFAM_1:def 2, A1, Th62;
assume b in X ; :: thesis: ex cc being set st
( a \/ b c= cc & cc in X )
then consider bb being set such that
A3: ( bb in B & b c= bb ) by SETFAM_1:def 2, A1, Th62;
consider cc being set such that
A4: ( aa \/ bb c= cc & cc in B ) by A1, A2, A3, COHSP_1:5;
take cc = cc; :: thesis: ( a \/ b c= cc & cc in X )
a \/ b c= aa \/ bb by A2, A3, XBOOLE_1:13;
hence a \/ b c= cc by A4; :: thesis: cc in X
thus cc in X by A4, XBOOLE_0:def 3; :: thesis: verum
end;
hence A \/ B is c=directed by COHSP_1:6; :: thesis: verum