let T1, T2 be TopStruct ; :: thesis: for T being Refinement of T1,T2
for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds
the topology of T = UniCl (FinMeetCl X)
let T be Refinement of T1,T2; :: thesis: for X being Subset-Family of T st X = the topology of T1 \/ the topology of T2 holds
the topology of T = UniCl (FinMeetCl X)
let X be Subset-Family of T; :: thesis: ( X = the topology of T1 \/ the topology of T2 implies the topology of T = UniCl (FinMeetCl X) )
assume X = the topology of T1 \/ the topology of T2 ; :: thesis: the topology of T = UniCl (FinMeetCl X)
then X is prebasis of T by Def6;
then FinMeetCl X is Basis of T by Th23;
hence the topology of T = UniCl (FinMeetCl X) by Th22; :: thesis: verum