let S be non empty Poset; :: thesis: for N being reflexive monotone net of S holds { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } is non empty directed Subset of S
let N be reflexive monotone net of S; :: thesis: { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } is non empty directed Subset of S
set X = { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } ;
consider jj being Element of N;
A1: "/\" { (N . i) where i is Element of N : i >= jj } ,S in { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } ;
{ ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } c= the carrier of S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } or x in the carrier of S )
assume x in { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } ; :: thesis: x in the carrier of S
then ex j being Element of N st x = "/\" { (N . i) where i is Element of N : i >= j } ,S ;
hence x in the carrier of S ; :: thesis: verum

end;

then reconsider X = { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } as non empty Subset of S by A1;
X is directed

proof

let x, y be Element of S; :: according to WAYBEL_0:def 1 :: thesis: ( not x in X or not y in X or ex b₁ being Element of the carrier of S st
( b₁ in X & x <= b₁ & y <= b₁ ) )
assume x in X ; :: thesis: ( not y in X or ex b₁ being Element of the carrier of S st
( b₁ in X & x <= b₁ & y <= b₁ ) )
then consider j1 being Element of N such that
A2: x = "/\" { (N . i) where i is Element of N : i >= j1 } ,S ;
assume y in X ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in X & x <= b₁ & y <= b₁ )
then consider j2 being Element of N such that
A3: y = "/\" { (N . i) where i is Element of N : i >= j2 } ,S ;
reconsider j1 = j1, j2 = j2 as Element of N ;
[#] N is directed by WAYBEL_0:def 6;
then consider j being Element of N such that
j in [#] N and
A4: j >= j1 and
A5: j >= j2 by WAYBEL_0:def 1;
set z = "/\" { (N . i) where i is Element of N : i >= j } ,S;
take "/\" { (N . i) where i is Element of N : i >= j } ,S ; :: thesis: ( "/\" { (N . i) where i is Element of N : i >= j } ,S in X & x <= "/\" { (N . i) where i is Element of N : i >= j } ,S & y <= "/\" { (N . i) where i is Element of N : i >= j } ,S )
thus "/\" { (N . i) where i is Element of N : i >= j } ,S in X ; :: thesis: ( x <= "/\" { (N . i) where i is Element of N : i >= j } ,S & y <= "/\" { (N . i) where i is Element of N : i >= j } ,S )
deffunc H₁( Element of N) -> set = { (N . i) where i is Element of N : i >= $1 } ;
A6: for j being Element of N holds ex_inf_of H₁(j),S

proof

let j be Element of N; :: thesis: ex_inf_of H₁(j),S
reconsider j9 = j as Element of N ;

now

take x = N . j; :: thesis: ( x is_<=_than H₁(j) & ( for y being Element of S st y is_<=_than H₁(j) holds
y <= x ) )
j9 <= j9 ;
then A7: x in H₁(j) ;
thus x is_<=_than H₁(j) :: thesis: for y being Element of S st y is_<=_than H₁(j) holds
y <= x

proof

let y be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not y in H₁(j) or x <= y )
assume y in H₁(j) ; :: thesis: x <= y
then ex i being Element of N st
( y = N . i & i >= j ) ;
hence x <= y by WAYBEL11:def 9; :: thesis: verum

end;

let y be Element of S; :: thesis: ( y is_<=_than H₁(j) implies y <= x )
assume y is_<=_than H₁(j) ; :: thesis: y <= x
hence y <= x by A7, LATTICE3:def 8; :: thesis: verum

end;

hence ex_inf_of H₁(j),S by YELLOW_0:16; :: thesis: verum

end;

then A8: ex_inf_of H₁(j1),S ;
A9: ex_inf_of H₁(j2),S by A6;
A10: ex_inf_of H₁(j),S by A6;
set A = { (N . i) where i is Element of N : i >= j } ;
{ (N . i) where i is Element of N : i >= j } c= { (N . k) where k is Element of N : k >= j1 }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (N . i) where i is Element of N : i >= j } or a in { (N . k) where k is Element of N : k >= j1 } )
assume a in { (N . i) where i is Element of N : i >= j } ; :: thesis: a in { (N . k) where k is Element of N : k >= j1 }
then consider k being Element of N such that
A11: a = N . k and
A12: k >= j ;
reconsider k = k as Element of N ;
k >= j1 by A4, A12, ORDERS_2:26;
hence a in { (N . k) where k is Element of N : k >= j1 } by A11; :: thesis: verum

end;

hence "/\" { (N . i) where i is Element of N : i >= j } ,S >= x by A2, A8, A10, YELLOW_0:35; :: thesis: y <= "/\" { (N . i) where i is Element of N : i >= j } ,S
{ (N . i) where i is Element of N : i >= j } c= { (N . k) where k is Element of N : k >= j2 }

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in { (N . i) where i is Element of N : i >= j } or a in { (N . k) where k is Element of N : k >= j2 } )
assume a in { (N . i) where i is Element of N : i >= j } ; :: thesis: a in { (N . k) where k is Element of N : k >= j2 }
then consider k being Element of N such that
A13: a = N . k and
A14: k >= j ;
reconsider k = k as Element of N ;
k >= j2 by A5, A14, ORDERS_2:26;
hence a in { (N . k) where k is Element of N : k >= j2 } by A13; :: thesis: verum

end;

hence y <= "/\" { (N . i) where i is Element of N : i >= j } ,S by A3, A9, A10, YELLOW_0:35; :: thesis: verum

end;

hence { ("/\" { (N . i) where i is Element of N : i >= j } ,S) where j is Element of N : verum } is non empty directed Subset of S ; :: thesis: verum