let R1, R2 be non empty reflexive RelStr ; :: thesis: ( RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) implies for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed )
assume A1: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ; :: thesis: for D being Subset of R1
for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
let D be Subset of R1; :: thesis: for D9 being Subset of R2 st D = D9 & D is directed holds
D9 is directed
let D9 be Subset of R2; :: thesis: ( D = D9 & D is directed implies D9 is directed )
assume that
A2: D = D9 and
A3: D is directed ; :: thesis: D9 is directed
let x2, y2 be Element of R2; :: according to WAYBEL_0:def 1 :: thesis: ( not x2 in D9 or not y2 in D9 or ex b₁ being Element of the carrier of R2 st
( b₁ in D9 & x2 <= b₁ & y2 <= b₁ ) )
assume that
A4: x2 in D9 and
A5: y2 in D9 ; :: thesis: ex b₁ being Element of the carrier of R2 st
( b₁ in D9 & x2 <= b₁ & y2 <= b₁ )
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
consider z1 being Element of R1 such that
A6: z1 in D and
A7: x1 <= z1 and
A8: y1 <= z1 by A2, A3, A4, A5;
reconsider z2 = z1 as Element of R2 by A1;
take z2 ; :: thesis: ( z2 in D9 & x2 <= z2 & y2 <= z2 )
thus z2 in D9 by A2, A6; :: thesis: ( x2 <= z2 & y2 <= z2 )
thus ( x2 <= z2 & y2 <= z2 ) by A1, A7, A8, Lm1; :: thesis: verum