set S = { [a,f] where a is Element of L, f is Element of F : a in f } ;

for x, y being Element of (a_net F) st x in [#] (a_net F) & y in [#] (a_net F) holds

ex z being Element of (a_net F) st

( z in [#] (a_net F) & x <= z & y <= z )

hence a_net F is directed ; :: thesis: verum

for x, y being Element of (a_net F) st x in [#] (a_net F) & y in [#] (a_net F) holds

ex z being Element of (a_net F) st

( z in [#] (a_net F) & x <= z & y <= z )

proof

then
[#] (a_net F) is directed
;
let x, y be Element of (a_net F); :: thesis: ( x in [#] (a_net F) & y in [#] (a_net F) implies ex z being Element of (a_net F) st

( z in [#] (a_net F) & x <= z & y <= z ) )

assume that

x in [#] (a_net F) and

y in [#] (a_net F) ; :: thesis: ex z being Element of (a_net F) st

( z in [#] (a_net F) & x <= z & y <= z )

x in the carrier of (a_net F) ;

then x in { [a,f] where a is Element of L, f is Element of F : a in f } by Def4;

then consider a being Element of L, f being Element of F such that

A1: x = [a,f] and

a in f ;

reconsider f = f as Element of (BoolePoset O) ;

y in the carrier of (a_net F) ;

then y in { [a,f] where a is Element of L, f is Element of F : a in f } by Def4;

then consider b being Element of L, g being Element of F such that

A2: y = [b,g] and

b in g ;

reconsider g = g as Element of (BoolePoset O) ;

reconsider h = f "/\" g as Element of F by WAYBEL_0:41;

set s = the Element of h;

A3: h c= O by WAYBEL_8:26;

not Bottom (BoolePoset O) in F by WAYBEL_7:4;

then not {} in F by YELLOW_1:18;

then A4: h <> {} ;

then the Element of h in h ;

then the Element of h in O by A3;

then reconsider s = the Element of h as Element of L ;

[s,h] in { [a,f] where a is Element of L, f is Element of F : a in f } by A4;

then reconsider z = [s,h] as Element of (a_net F) by Def4;

reconsider i = x, j = y, k = z as Element of (a_net F) ;

A5: [b,g] `2 = g ;

take z ; :: thesis: ( z in [#] (a_net F) & x <= z & y <= z )

A6: [s,h] `2 = h ;

f /\ g c= g by XBOOLE_1:17;

then A7: h c= g by YELLOW_1:17;

f /\ g c= f by XBOOLE_1:17;

then A8: h c= f by YELLOW_1:17;

[a,f] `2 = f ;

hence ( z in [#] (a_net F) & x <= z & y <= z ) by A5, A6, A8, A7, Def4, A1, A2; :: thesis: verum

end;( z in [#] (a_net F) & x <= z & y <= z ) )

assume that

x in [#] (a_net F) and

y in [#] (a_net F) ; :: thesis: ex z being Element of (a_net F) st

( z in [#] (a_net F) & x <= z & y <= z )

x in the carrier of (a_net F) ;

then x in { [a,f] where a is Element of L, f is Element of F : a in f } by Def4;

then consider a being Element of L, f being Element of F such that

A1: x = [a,f] and

a in f ;

reconsider f = f as Element of (BoolePoset O) ;

y in the carrier of (a_net F) ;

then y in { [a,f] where a is Element of L, f is Element of F : a in f } by Def4;

then consider b being Element of L, g being Element of F such that

A2: y = [b,g] and

b in g ;

reconsider g = g as Element of (BoolePoset O) ;

reconsider h = f "/\" g as Element of F by WAYBEL_0:41;

set s = the Element of h;

A3: h c= O by WAYBEL_8:26;

not Bottom (BoolePoset O) in F by WAYBEL_7:4;

then not {} in F by YELLOW_1:18;

then A4: h <> {} ;

then the Element of h in h ;

then the Element of h in O by A3;

then reconsider s = the Element of h as Element of L ;

[s,h] in { [a,f] where a is Element of L, f is Element of F : a in f } by A4;

then reconsider z = [s,h] as Element of (a_net F) by Def4;

reconsider i = x, j = y, k = z as Element of (a_net F) ;

A5: [b,g] `2 = g ;

take z ; :: thesis: ( z in [#] (a_net F) & x <= z & y <= z )

A6: [s,h] `2 = h ;

f /\ g c= g by XBOOLE_1:17;

then A7: h c= g by YELLOW_1:17;

f /\ g c= f by XBOOLE_1:17;

then A8: h c= f by YELLOW_1:17;

[a,f] `2 = f ;

hence ( z in [#] (a_net F) & x <= z & y <= z ) by A5, A6, A8, A7, Def4, A1, A2; :: thesis: verum

hence a_net F is directed ; :: thesis: verum