let S be complete LATTICE; :: thesis: for N being net of holds { ("/\" { (N . i) where i is Element of : i >= j } ,S) where j is Element of : verum } is non empty directed Subset of
let N be net of ; :: thesis: { ("/\" { (N . i) where i is Element of : i >= j } ,S) where j is Element of : verum } is non empty directed Subset of
set X = { ("/\" { (N . i) where i is Element of : i >= j } ,S) where j is Element of : verum } ;
{ ("/\" { (N . i) where i is Element of : i >= j } ,S) where j is Element of : 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 : i >= j } ,S) where j is Element of : verum } or x in the carrier of S )
assume x in { ("/\" { (N . i) where i is Element of : i >= j } ,S) where j is Element of : verum } ; :: thesis: x in the carrier of S
then ex j being Element of st x = "/\" { (N . i) where i is Element of : i >= j } ,S ;
hence x in the carrier of S ; :: thesis: verum

end;

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