let A, B, Y, X be set ; :: thesis: ( A is_finer_than B & X is_finer_than Y implies A \/ X is_finer_than B \/ Y )
set LH = A \/ X;
set RH = B \/ Y;
assume A1: ( A is_finer_than B & X is_finer_than Y ) ; :: thesis: A \/ X is_finer_than B \/ Y
now :: thesis: for Z being set st Z in A \/ X holds
ex b being set st
( b in B \/ Y & Z c= b )
let Z be set ; :: thesis: ( Z in A \/ X implies ex b being set st
( b2 in B \/ Y & b c= b2 ) )
assume A2: Z in A \/ X ; :: thesis: ex b being set st
( b2 in B \/ Y & b c= b2 )
per cases ( Z in A or Z in X ) by XBOOLE_0:def 3, A2;
suppose Z in A ; :: thesis: ex b being set st
( b2 in B \/ Y & b c= b2 )
then consider b being set such that
A3: ( b in B & Z c= b ) by SETFAM_1:def 2, A1;
take b = b; :: thesis: ( b in B \/ Y & Z c= b )
thus b in B \/ Y by A3, XBOOLE_0:def 3; :: thesis: Z c= b
thus Z c= b by A3; :: thesis: verum
end;
suppose Z in X ; :: thesis: ex y being set st
( b2 in B \/ Y & y c= b2 )
then consider y being set such that
A4: ( y in Y & Z c= y ) by SETFAM_1:def 2, A1;
take y = y; :: thesis: ( y in B \/ Y & Z c= y )
thus y in B \/ Y by A4, XBOOLE_0:def 3; :: thesis: Z c= y
thus Z c= y by A4; :: thesis: verum
end;
end;
end;
hence A \/ X is_finer_than B \/ Y by SETFAM_1:def 2; :: thesis: verum