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 )
proof
let x,
y be
Element of
(a_net F);
( 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)
;
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
;
( 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;
verum
end;
then
[#] (a_net F) is directed
;
hence
a_net F is directed
; verum