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