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 that
A2: x in X and
A3: y in X ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in X & x <= b₁ & y <= b₁ )
consider z being Element of L such that
A4: z in X and
A5: [x,z] in the InternalRel of L and
A6: [y,z] in the InternalRel of L by A1, A2, A3;
take z ; :: thesis: ( z in X & x <= z & y <= z )
thus z in X by A4; :: thesis: ( x <= z & y <= z )
thus ( x <= z & y <= z ) by A5, A6, ORDERS_2:def 5; :: thesis: verum