let T be non empty TopSpace; :: thesis: Top (Open_setLatt T) = the carrier of T

set OL = Open_setLatt T;

reconsider B = the carrier of T as Element of (Open_setLatt T) by PRE_TOPC:def 1;

set OL = Open_setLatt T;

reconsider B = the carrier of T as Element of (Open_setLatt T) by PRE_TOPC:def 1;

now :: thesis: for p being Element of (Open_setLatt T) holds

( B "\/" p = B & p "\/" B = B )

hence
Top (Open_setLatt T) = the carrier of T
by LATTICES:def 17; :: thesis: verum( B "\/" p = B & p "\/" B = B )

let p be Element of (Open_setLatt T); :: thesis: ( B "\/" p = B & p "\/" B = B )

reconsider p9 = p as Element of Topology_of T ;

thus B "\/" p = the carrier of T \/ p9 by Def2

.= B by XBOOLE_1:12 ; :: thesis: p "\/" B = B

hence p "\/" B = B ; :: thesis: verum

end;reconsider p9 = p as Element of Topology_of T ;

thus B "\/" p = the carrier of T \/ p9 by Def2

.= B by XBOOLE_1:12 ; :: thesis: p "\/" B = B

hence p "\/" B = B ; :: thesis: verum