let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies for X1 being Subset of L1

for X2 being Subset of L2 st X1 = X2 & X1 is directed holds

X2 is directed )

assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for X1 being Subset of L1

for X2 being Subset of L2 st X1 = X2 & X1 is directed holds

X2 is directed

let X1 be Subset of L1; :: thesis: for X2 being Subset of L2 st X1 = X2 & X1 is directed holds

X2 is directed

let X2 be Subset of L2; :: thesis: ( X1 = X2 & X1 is directed implies X2 is directed )

assume A2: X1 = X2 ; :: thesis: ( not X1 is directed or X2 is directed )

assume A3: for x, y being Element of L1 st x in X1 & y in X1 holds

ex z being Element of L1 st

( z in X1 & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: X2 is directed

let x, y be Element of L2; :: according to WAYBEL_0:def 1 :: thesis: ( x in X2 & y in X2 implies ex z being Element of L2 st

( z in X2 & x <= z & y <= z ) )

reconsider x9 = x, y9 = y as Element of L1 by A1;

assume that

A4: x in X2 and

A5: y in X2 ; :: thesis: ex z being Element of L2 st

( z in X2 & x <= z & y <= z )

consider z9 being Element of L1 such that

A6: z9 in X1 and

A7: x9 <= z9 and

A8: y9 <= z9 by A2, A3, A4, A5;

reconsider z = z9 as Element of L2 by A1;

take z ; :: thesis: ( z in X2 & x <= z & y <= z )

thus ( z in X2 & x <= z & y <= z ) by A1, A2, A6, A7, A8, YELLOW_0:1; :: thesis: verum

for X2 being Subset of L2 st X1 = X2 & X1 is directed holds

X2 is directed )

assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: for X1 being Subset of L1

for X2 being Subset of L2 st X1 = X2 & X1 is directed holds

X2 is directed

let X1 be Subset of L1; :: thesis: for X2 being Subset of L2 st X1 = X2 & X1 is directed holds

X2 is directed

let X2 be Subset of L2; :: thesis: ( X1 = X2 & X1 is directed implies X2 is directed )

assume A2: X1 = X2 ; :: thesis: ( not X1 is directed or X2 is directed )

assume A3: for x, y being Element of L1 st x in X1 & y in X1 holds

ex z being Element of L1 st

( z in X1 & x <= z & y <= z ) ; :: according to WAYBEL_0:def 1 :: thesis: X2 is directed

let x, y be Element of L2; :: according to WAYBEL_0:def 1 :: thesis: ( x in X2 & y in X2 implies ex z being Element of L2 st

( z in X2 & x <= z & y <= z ) )

reconsider x9 = x, y9 = y as Element of L1 by A1;

assume that

A4: x in X2 and

A5: y in X2 ; :: thesis: ex z being Element of L2 st

( z in X2 & x <= z & y <= z )

consider z9 being Element of L1 such that

A6: z9 in X1 and

A7: x9 <= z9 and

A8: y9 <= z9 by A2, A3, A4, A5;

reconsider z = z9 as Element of L2 by A1;

take z ; :: thesis: ( z in X2 & x <= z & y <= z )

thus ( z in X2 & x <= z & y <= z ) by A1, A2, A6, A7, A8, YELLOW_0:1; :: thesis: verum