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

proof

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₁ being Element of the carrier of L st
( b₁ in C & b₁ <= x & b₁ <= y ) )
A2: ( x <= x & y <= y ) ;
assume A3: ( x in C & y in C ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in C & b₁ <= x & b₁ <= 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₁ being Element of the carrier of L st
( b₁ in C & b₁ <= x & b₁ <= y ) by A3, A2; :: thesis: verum

end;

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₁ being Element of the carrier of L st
( b₁ in C & x <= b₁ & y <= b₁ ) )
A4: ( x <= x & y <= y ) ;
assume A5: ( x in C & y in C ) ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in C & x <= b₁ & y <= 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₁ being Element of the carrier of L st
( b₁ in C & x <= b₁ & y <= b₁ ) by A5, A4; :: thesis: verum