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 :: thesis: for y being Element of (I /\/ FI) holds
( ((Top I) /\/ FI) "\/" y = (Top I) /\/ FI & y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI )

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:36;
A3: (Top I) "\/" j = Top I ;
A4: y = j /\/ FI by A2, Def6;
hence ((Top I) /\/ FI) "\/" y = (Top I) /\/ FI by A3, Th15; :: thesis: y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI
thus y "\/" ((Top I) /\/ FI) = (Top I) /\/ FI by A3, A4, 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