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 )
A1: a => a = Top B by Th28;
( i => i = Top I & (Top I) "/\" (Top I) = Top I ) by Th28;
hence ( i <=> i in FI & a <=> a in FB ) by A1, Th11; :: according to FILTER_0:def 12 :: thesis: verum