let L be RelStr ; :: thesis: for X being Subset of L st X is_directed_wrt the InternalRel of L holds
X is directed
let X be Subset of L; :: thesis: ( X is_directed_wrt the InternalRel of L implies X is directed )
assume A1: X is_directed_wrt the InternalRel of L ; :: thesis: X is directed
let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not x in X or not y in X or ex b₁ being Element of the carrier of L st
( b₁ in X & x <= b₁ & y <= b₁ ) )
assume ( x in X & y in X ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in X & x <= b₁ & y <= b₁ )
then consider z being Element of L such that
A2: ( z in X & [x,z] in the InternalRel of L & [y,z] in the InternalRel of L ) by A1, Def23;
take z ; :: thesis: ( z in X & x <= z & y <= z )
thus z in X by A2; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A2, ORDERS_2:def 9; :: thesis: verum