let V, A be set ; :: thesis: for d1, d2 being TypeSCNominativeData of V,A holds d2 c= global_overlapping (V,A,d1,d2)
let d1, d2 be TypeSCNominativeData of V,A; :: thesis: d2 c= global_overlapping (V,A,d1,d2)

per cases ( ( not d1 in A & not d2 in A ) or d1 in A or d2 in A ) ;

suppose ( not d1 in A & not d2 in A ) ; :: thesis: d2 c= global_overlapping (V,A,d1,d2)

then ex f1, f2 being Function st
( f1 = d1 & f2 = d2 & global_overlapping (V,A,d1,d2) = f2 \/ (f1 | ((dom f1) \ (dom f2))) ) by NOMIN_1:def 16;
hence d2 c= global_overlapping (V,A,d1,d2) by XBOOLE_1:7; :: thesis: verum

end;

suppose ( d1 in A or d2 in A ) ; :: thesis: d2 c= global_overlapping (V,A,d1,d2)

hence d2 c= global_overlapping (V,A,d1,d2) by NOMIN_1:def 16; :: thesis: verum

end;

end;