let T be non empty TopRelStr ; :: thesis: ( T is naturally_generated implies for A being Subset of T holds
( A is open iff LAp A = A ) )
assume A1: T is naturally_generated ; :: thesis: for A being Subset of T holds
( A is open iff LAp A = A )
let A be Subset of T; :: thesis: ( A is open iff LAp A = A )
thus ( A is open implies LAp A = A ) :: thesis: ( LAp A = A implies A is open )
proof
assume A is open ; :: thesis: LAp A = A
then A in GenTop (LAp T) by A1, PRE_TOPC:def 2;
then ex S being Subset of T st
( S = A & S is LAp T -closed ) by GTDef;
hence LAp A = A by ROUGHS_2:def 10; :: thesis: verum
end;
assume LAp A = A ; :: thesis: A is open
then A is LAp T -closed by ROUGHS_2:def 10;
then A in GenTop (LAp T) by GTDef;
hence A is open by PRE_TOPC:def 2, A1; :: thesis: verum