let N be complete Lawson TopLattice; :: thesis: for X being Subset of N holds
( X in lambda N iff X is open )
let X be Subset of N; :: thesis: ( X in lambda N iff X is open )
lambda N = the topology of N by Th9;
hence ( X in lambda N iff X is open ) by PRE_TOPC:def 5; :: thesis: verum