let N be complete Lawson TopLattice; :: thesis: for X being Subset of holds
( X in lambda N iff X is open )
let X be Subset of ; :: 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