set X = [:D1,D2:];
[:D1,D2:] is directed
proof
let x,
y be
Element of
[:S1,S2:];
WAYBEL_0:def 1 ( not x in [:D1,D2:] or not y in [:D1,D2:] or ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & x <= b1 & y <= b1 ) )
assume that A1:
x in [:D1,D2:]
and A2:
y in [:D1,D2:]
;
ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & x <= b1 & y <= b1 )
consider x1,
x2 being
object such that A3:
x1 in D1
and A4:
x2 in D2
and A5:
x = [x1,x2]
by A1, ZFMISC_1:def 2;
reconsider S29 =
S2 as non
empty RelStr by A4;
reconsider S19 =
S1 as non
empty RelStr by A3;
consider y1,
y2 being
object such that A6:
y1 in D1
and A7:
y2 in D2
and A8:
y = [y1,y2]
by A2, ZFMISC_1:def 2;
reconsider x2 =
x2,
y2 =
y2 as
Element of
S2 by A4, A7;
consider xy2 being
Element of
S2 such that A9:
xy2 in D2
and A10:
(
x2 <= xy2 &
y2 <= xy2 )
by A4, A7, WAYBEL_0:def 1;
reconsider x1 =
x1,
y1 =
y1 as
Element of
S1 by A3, A6;
consider xy1 being
Element of
S1 such that A11:
xy1 in D1
and A12:
(
x1 <= xy1 &
y1 <= xy1 )
by A3, A6, WAYBEL_0:def 1;
reconsider xy29 =
xy2 as
Element of
S29 ;
reconsider xy19 =
xy1 as
Element of
S19 ;
[xy19,xy29] is
Element of
[:S19,S29:]
;
then reconsider z =
[xy1,xy2] as
Element of
[:S1,S2:] ;
take
z
;
( z in [:D1,D2:] & x <= z & y <= z )
thus
z in [:D1,D2:]
by A11, A9, ZFMISC_1:87;
( x <= z & y <= z )
( not
S1 is
empty & not
S2 is
empty )
by A3, A4;
hence
(
x <= z &
y <= z )
by A5, A8, A12, A10, Th11;
verum
end;
hence
for b1 being Subset of [:S1,S2:] st b1 = [:D1,D2:] holds
b1 is directed
; verum