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 } ;
set jj = the Element of N;
A1: "/\" ( { (N . i) where i is Element of N : i >= the Element of N } ,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 object ; :: 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 b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 ) )
assume x in X ; :: thesis: ( not y in X or ex b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 ) )
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 b1 being Element of the carrier of S st
( b1 in X & x <= b1 & y <= b1 )
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 ;
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 H1( 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 H1(j),S
proof
let j be Element of N; :: thesis: ex_inf_of H1(j),S
reconsider j9 = j as Element of N ;
now :: thesis: ex x being Element of the carrier of S st
( x is_<=_than H1(j) & ( for y being Element of S st y is_<=_than H1(j) holds
y <= x ) )
take x = N . j; :: thesis: ( x is_<=_than H1(j) & ( for y being Element of S st y is_<=_than H1(j) holds
y <= x ) )
j9 <= j9 ;
then A7: x in H1(j) ;
thus x is_<=_than H1(j) :: thesis: for y being Element of S st y is_<=_than H1(j) holds
y <= x
proof
let y be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not y in H1(j) or x <= y )
assume y in H1(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 H1(j) implies y <= x )
assume y is_<=_than H1(j) ; :: thesis: y <= x
hence y <= x by A7; :: thesis: verum
end;
hence ex_inf_of H1(j),S by YELLOW_0:16; :: thesis: verum
end;
then A8: ex_inf_of H1(j1),S ;
A9: ex_inf_of H1(j2),S by A6;
A10: ex_inf_of H1(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 object ; :: 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:3;
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 object ; :: 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:3;
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