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);
:: 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
(
x in [#] (a_net F) &
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) &
y in the
carrier of
(a_net F) )
;
then A1:
(
x in { [a,f] where a is Element of L, f is Element of F : a in f } &
y 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 A2:
(
x = [a,f] &
a in f )
;
consider b being
Element of
L,
g being
Element of
F such that A3:
(
y = [b,g] &
b in g )
by A1;
reconsider f =
f as
Element of
(BoolePoset O) ;
reconsider g =
g as
Element of
(BoolePoset O) ;
reconsider h =
f "/\" g as
Element of
F by WAYBEL_0:41;
consider s being
Element of
h;
not
Bottom (BoolePoset O) in F
by WAYBEL_7:8;
then
not
{} in F
by YELLOW_1:18;
then A4:
h <> {}
;
then A5:
s in h
;
h c= O
by WAYBEL_8:28;
then
s in O
by A5;
then reconsider s =
s as
Element of
L ;
A6:
[s,h] in { [a,f] where a is Element of L, f is Element of F : a in f }
by A4;
reconsider z =
[s,h] as
Element of
(a_net F) by A6, Def4;
reconsider i =
x,
j =
y,
k =
z as
Element of
(a_net F) ;
A8:
(
i `2 = f &
j `2 = g &
k `2 = h )
by A2, A3, MCART_1:def 2;
(
h c= f /\ g &
f /\ g c= f &
f /\ g c= g )
by XBOOLE_1:17, YELLOW_1:17;
then A9:
(
h c= f &
h c= g )
by XBOOLE_1:1;
take
z
;
:: thesis: ( z in [#] (a_net F) & x <= z & y <= z )
thus
(
z in [#] (a_net F) &
x <= z &
y <= z )
by A8, A9, Def4;
:: thesis: verum
end;
then
[#] (a_net F) is directed
by WAYBEL_0:def 1;
hence
a_net F is directed
by WAYBEL_0:def 6; :: thesis: verum