let I be set ; :: thesis: [#] (OrderedFIN I) is directed
A1: the carrier of (OrderedFIN I) = Fin I by YELLOW_1:1;
then A2: [#] (OrderedFIN I) = Fin I by STRUCT_0:def 3;

now :: thesis: for a, b being Element of (OrderedFIN I) st a in [#] (OrderedFIN I) & b in [#] (OrderedFIN I) holds
ex z being Element of (OrderedFIN I) st
( z in [#] (OrderedFIN I) & a <= z & b <= z )

let a, b be Element of (OrderedFIN I); :: thesis: ( a in [#] (OrderedFIN I) & b in [#] (OrderedFIN I) implies ex z being Element of (OrderedFIN I) st
( z in [#] (OrderedFIN I) & a <= z & b <= z ) )
assume that
a in [#] (OrderedFIN I) and
b in [#] (OrderedFIN I) ; :: thesis: ex z being Element of (OrderedFIN I) st
( z in [#] (OrderedFIN I) & a <= z & b <= z )
reconsider z = a \/ b as Element of (OrderedFIN I) by A1, FINSUB_1:def 1;
take z = z; :: thesis: ( z in [#] (OrderedFIN I) & a <= z & b <= z )
thus ( z in [#] (OrderedFIN I) & a <= z & b <= z ) by A1, A2, YELLOW_1:3, XBOOLE_1:7; :: thesis: verum

end;

hence [#] (OrderedFIN I) is directed by WAYBEL_0:def 1; :: thesis: verum