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:
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:
then reconsider K = subrelstr A as infs-inheriting SubRelStr of T by ;
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:
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:
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