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;

now :: thesis: for p being Element of (Open_setLatt T) holds
( 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;

hence Top (Open_setLatt T) = the carrier of T by LATTICES:def 17; :: thesis: verum