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;

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 )

hence
[#] (OrderedFIN I) is directed
by WAYBEL_0:def 1; :: thesis: verumex 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;( 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