let S be complete LATTICE; :: thesis: for N being 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 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 } ;
{ ("/\" ( { (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 Subset of S ;
( not X is empty & X is directed ) by WAYBEL11:30;
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