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};

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

A7:
W is with_open_semilattices
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;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

proof

W is with_small_semilattices
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;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

proof

hence
( T is with_small_semilattices & T is with_open_semilattices )
by A7; :: thesis: verum
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;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