let B be B_Lattice; :: thesis: for FB being Filter of B
for I being I_Lattice
for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let FB be Filter of B; :: thesis: for I being I_Lattice
for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let I be I_Lattice; :: thesis: for i being Element of I
for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let i be Element of I; :: thesis: for FI being Filter of I
for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let FI be Filter of I; :: thesis: for a being Element of B holds
( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
let a be Element of B; :: thesis: ( i,i are_equivalence_wrt FI & a,a are_equivalence_wrt FB )
B is I_Lattice by Th40;
then ( i => i = Top I & a => a = Top B ) by Th38;
then A1: ( i <=> i = (Top I) "/\" (Top I) & a <=> a = (Top B) "/\" (Top B) & (Top I) "/\" (Top I) = Top I & (Top B) "/\" (Top B) = Top B ) by LATTICES:18;
( I is 1_Lattice & B is 1_Lattice ) by Th37;
hence ( i <=> i in FI & a <=> a in FB ) by A1, Th12; :: according to FILTER_0:def 13 :: thesis: verum