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;

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

( 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 )

hence
I /\/ FI is 1_Lattice
by LATTICES:def 14; :: thesis: Top (I /\/ FI) = (Top I) /\/ FI( ((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;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

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