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 D' being Subset of R2 st D = D' & D is directed holds
D' 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 D' being Subset of R2 st D = D' & D is directed holds
D' is directed
let D be Subset of R1; :: thesis: for D' being Subset of R2 st D = D' & D is directed holds
D' is directed
let D' be Subset of R2; :: thesis: ( D = D' & D is directed implies D' is directed )
assume that
A2: D = D' and
A3: D is directed ; :: thesis: D' is directed
let x2, y2 be Element of R2; :: according to WAYBEL_0:def 1 :: thesis: ( not x2 in D' or not y2 in D' or ex b₁ being Element of the carrier of R2 st
( b₁ in D' & x2 <= b₁ & y2 <= b₁ ) )
assume A4: ( x2 in D' & y2 in D' ) ; :: thesis: ex b₁ being Element of the carrier of R2 st
( b₁ in D' & x2 <= b₁ & y2 <= b₁ )
reconsider x1 = x2, y1 = y2 as Element of R1 by A1;
consider z1 being Element of R1 such that
A5: z1 in D and
A6: ( x1 <= z1 & y1 <= z1 ) by A2, A3, A4, WAYBEL_0:def 1;
reconsider z2 = z1 as Element of R2 by A1;
take z2 ; :: thesis: ( z2 in D' & x2 <= z2 & y2 <= z2 )
thus z2 in D' by A2, A5; :: thesis: ( x2 <= z2 & y2 <= z2 )
thus ( x2 <= z2 & y2 <= z2 ) by A1, A6, Lm1; :: thesis: verum