let X be TopStruct ; :: thesis: for F being Subset-Family of X holds
( F is open iff F c= the topology of X )
let F be Subset-Family of X; :: thesis: ( F is open iff F c= the topology of X )
thus ( F is open implies F c= the topology of X ) :: thesis: ( F c= the topology of X implies F is open )
proof
assume A1: F is open ; :: thesis: F c= the topology of X
let A be object ; :: according to TARSKI:def 3 :: thesis: ( not A in F or A in the topology of X )
assume A2: A in F ; :: thesis: A in the topology of X
then reconsider A = A as Subset of X ;
A is open by A1, A2;
hence A in the topology of X ; :: thesis: verum
end;
assume A3: F c= the topology of X ; :: thesis: F is open
let A be Subset of X; :: according to TOPS_2:def 1 :: thesis: ( A in F implies A is open )
thus ( A in F implies A is open ) by A3; :: thesis: verum