let T be non empty TopRelStr ; :: thesis: ( T is anti-discrete implies ( T is with_small_semilattices & T is with_open_semilattices ) )
assume T is anti-discrete ; :: thesis: ( T is with_small_semilattices & T is with_open_semilattices )
then reconsider W = T as non empty anti-discrete TopRelStr ;
set J = { the carrier of W};

A5: now :: thesis: for A being Subset of W st A in { the carrier of W} holds
subrelstr A is meet-inheriting

let A be Subset of W; :: thesis: ( A in { the carrier of W} implies subrelstr A is meet-inheriting )
A6: subrelstr ([#] W) is infs-inheriting ;
assume A in { the carrier of W} ; :: thesis: subrelstr A is meet-inheriting
then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by A6, TARSKI:def 1;
K is meet-inheriting ;
hence subrelstr A is meet-inheriting ; :: thesis: verum

end;

A7: W is with_open_semilattices

proof

let x be Point of W; :: according to WAYBEL30:def 4 :: thesis: ex J being Basis of x st
for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
reconsider J = { the carrier of W} as Basis of x by YELLOW13:13;
take J ; :: thesis: for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
let A be Subset of W; :: thesis: ( A in J implies subrelstr A is meet-inheriting )
assume A in J ; :: thesis: subrelstr A is meet-inheriting
hence subrelstr A is meet-inheriting by A5; :: thesis: verum

end;

W is with_small_semilattices

proof

let x be Point of W; :: according to WAYBEL30:def 2 :: thesis: ex J being basis of x st
for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
reconsider J = { the carrier of W} as basis of x by YELLOW13:21;
take J ; :: thesis: for A being Subset of W st A in J holds
subrelstr A is meet-inheriting
let A be Subset of W; :: thesis: ( A in J implies subrelstr A is meet-inheriting )
assume A in J ; :: thesis: subrelstr A is meet-inheriting
hence subrelstr A is meet-inheriting by A5; :: thesis: verum

end;

hence ( T is with_small_semilattices & T is with_open_semilattices ) by A7; :: thesis: verum