let S1, S2 be non empty RelStr ; :: thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds
( D1 is directed & D2 is directed )
let D1 be non empty Subset of S1; :: thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds
( D1 is directed & D2 is directed )
let D2 be non empty Subset of S2; :: thesis: ( [:D1,D2:] is directed implies ( D1 is directed & D2 is directed ) )
assume A1: [:D1,D2:] is directed ; :: thesis: ( D1 is directed & D2 is directed )
thus D1 is directed :: thesis: D2 is directed

proof

consider q1 being Element of D2;
let x, y be Element of S1; :: according to WAYBEL_0:def 1 :: thesis: ( not x in D1 or not y in D1 or ex b₁ being Element of the carrier of S1 st
( b₁ in D1 & x <= b₁ & y <= b₁ ) )
assume ( x in D1 & y in D1 ) ; :: thesis: ex b₁ being Element of the carrier of S1 st
( b₁ in D1 & x <= b₁ & y <= b₁ )
then ( [x,q1] in [:D1,D2:] & [y,q1] in [:D1,D2:] ) by ZFMISC_1:106;
then consider z being Element of [:S1,S2:] such that
A2: z in [:D1,D2:] and
A3: ( [x,q1] <= z & [y,q1] <= z ) by A1, WAYBEL_0:def 1;
reconsider z2 = z `2 as Element of D2 by A2, MCART_1:10;
reconsider zz = z `1 as Element of D1 by A2, MCART_1:10;
take zz ; :: thesis: ( zz in D1 & x <= zz & y <= zz )
thus zz in D1 ; :: thesis: ( x <= zz & y <= zz )
ex x, y being set st
( x in D1 & y in D2 & z = [x,y] ) by A2, ZFMISC_1:def 2;
then ( [x,q1] <= [zz,z2] & [y,q1] <= [zz,z2] ) by A3, MCART_1:8;
hence ( x <= zz & y <= zz ) by Th11; :: thesis: verum

end;

consider q1 being Element of D1;
let x, y be Element of S2; :: according to WAYBEL_0:def 1 :: thesis: ( not x in D2 or not y in D2 or ex b₁ being Element of the carrier of S2 st
( b₁ in D2 & x <= b₁ & y <= b₁ ) )
assume ( x in D2 & y in D2 ) ; :: thesis: ex b₁ being Element of the carrier of S2 st
( b₁ in D2 & x <= b₁ & y <= b₁ )
then ( [q1,x] in [:D1,D2:] & [q1,y] in [:D1,D2:] ) by ZFMISC_1:106;
then consider z being Element of [:S1,S2:] such that
A4: z in [:D1,D2:] and
A5: ( [q1,x] <= z & [q1,y] <= z ) by A1, WAYBEL_0:def 1;
reconsider z2 = z `1 as Element of D1 by A4, MCART_1:10;
reconsider zz = z `2 as Element of D2 by A4, MCART_1:10;
take zz ; :: thesis: ( zz in D2 & x <= zz & y <= zz )
thus zz in D2 ; :: thesis: ( x <= zz & y <= zz )
ex x, y being set st
( x in D1 & y in D2 & z = [x,y] ) by A4, ZFMISC_1:def 2;
then ( [q1,x] <= [z2,zz] & [q1,y] <= [z2,zz] ) by A5, MCART_1:8;
hence ( x <= zz & y <= zz ) by Th11; :: thesis: verum