let C be Chain of L; :: thesis: ( C is filtered & C is directed )

A1: the InternalRel of L is_strongly_connected_in C by ORDERS_2:def 7;

thus C is filtered :: thesis: C is directed_{1} being Element of the carrier of L st

( b_{1} in C & x <= b_{1} & y <= b_{1} ) )

A4: ( x <= x & y <= y ) ;

assume A5: ( x in C & y in C ) ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in C & x <= b_{1} & y <= b_{1} )

then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1;

then ( x <= y or y <= x ) by ORDERS_2:def 5;

hence ex b_{1} being Element of the carrier of L st

( b_{1} in C & x <= b_{1} & y <= b_{1} )
by A5, A4; :: thesis: verum

A1: the InternalRel of L is_strongly_connected_in C by ORDERS_2:def 7;

thus C is filtered :: thesis: C is directed

proof

let x, y be Element of L; :: according to WAYBEL_0:def 1 :: thesis: ( not x in C or not y in C or ex b
let x, y be Element of L; :: according to WAYBEL_0:def 2 :: thesis: ( not x in C or not y in C or ex b_{1} being Element of the carrier of L st

( b_{1} in C & b_{1} <= x & b_{1} <= y ) )

A2: ( x <= x & y <= y ) ;

assume A3: ( x in C & y in C ) ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in C & b_{1} <= x & b_{1} <= y )

then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1;

then ( x <= y or y <= x ) by ORDERS_2:def 5;

hence ex b_{1} being Element of the carrier of L st

( b_{1} in C & b_{1} <= x & b_{1} <= y )
by A3, A2; :: thesis: verum

end;( b

A2: ( x <= x & y <= y ) ;

assume A3: ( x in C & y in C ) ; :: thesis: ex b

( b

then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1;

then ( x <= y or y <= x ) by ORDERS_2:def 5;

hence ex b

( b

( b

A4: ( x <= x & y <= y ) ;

assume A5: ( x in C & y in C ) ; :: thesis: ex b

( b

then ( [x,y] in the InternalRel of L or [y,x] in the InternalRel of L ) by A1;

then ( x <= y or y <= x ) by ORDERS_2:def 5;

hence ex b

( b