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 ()),( the L_join of I /\/ ()),( the L_meet of I /\/ ()) #) by Def5;
then consider j being Element of I such that
A2: y = Class ((),j) by EQREL_1:36;
A3: (Top I) "\/" j = Top I ;
A4: y = j /\/ FI by ;
hence ((Top I) /\/ FI) "\/" y = (Top I) /\/ FI by ; :: 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 ; :: thesis: verum