reconsider S2 = [#] Y2 as directed Subset of by WAYBEL_0:def 6;
reconsider S1 = [#] Y1 as directed Subset of by WAYBEL_0:def 6;
[:S1,S2:] is directed ;
then [#] [:Y1,Y2:] is directed by YELLOW_3:def 2;
hence [:Y1,Y2:] is directed by WAYBEL_0:def 6; :: thesis: verum