let I be I_Lattice; :: thesis: for FI being Filter of I holds
( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )
let FI be Filter of I; :: thesis: ( I /\/ FI is 1_Lattice & Top (I /\/ FI) = (Top I) /\/ FI )
set L = I /\/ FI;
set R = equivalence_wrt FI;
set x = (Top I) /\/ FI;

A1: now

let y be Element of (I /\/ FI); :: thesis: ( ((Top I) /\/ FI) "\/" y = (Top I) /\/ FI & y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI )
I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),(the L_join of I /\/ (equivalence_wrt FI)),(the L_meet of I /\/ (equivalence_wrt FI)) #) by Def5;
then consider j being Element of I such that
A2: y = Class (equivalence_wrt FI),j by EQREL_1:45;
I is 1_Lattice by FILTER_0:37;
then A3: ( (Top I) "\/" j = Top I & y = j /\/ FI ) by A2, Def6, LATTICES:44;
hence ((Top I) /\/ FI) "\/" y = (Top I) /\/ FI by Th15; :: thesis: y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI
thus y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI by A3, Th15; :: thesis: verum

end;

hence I /\/ FI is 1_Lattice by LATTICES:def 14; :: thesis: Top (I /\/ FI) = (Top I) /\/ FI
hence Top (I /\/ FI) = (Top I) /\/ FI by A1, LATTICES:def 17; :: thesis: verum