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
for D' being Subset of 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
for D' being Subset of st D = D' & D is directed holds
D' is directed
let D be Subset of ; :: thesis: for D' being Subset of st D = D' & D is directed holds
D' is directed
let D' be Subset of ; :: 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 ; :: 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 that
A4: x2 in D' and
A5: 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 by A1;
consider z1 being Element of such that
A6: z1 in D and
A7: x1 <= z1 and
A8: y1 <= z1 by A2, A3, A4, A5, WAYBEL_0:def 1;
reconsider z2 = z1 as Element of by A1;
take z2 ; :: thesis: ( z2 in D' & x2 <= z2 & y2 <= z2 )
thus z2 in D' by A2, A6; :: thesis: ( x2 <= z2 & y2 <= z2 )
thus ( x2 <= z2 & y2 <= z2 ) by A1, A7, A8, Lm1; :: thesis: verum