let X be BCI-algebra; :: thesis: for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K
for w being Element of Union G,RK ex a being Element of G st w in Class RK,a
let G be SubAlgebra of X; :: thesis: for K being closed Ideal of X
for RK being I-congruence of X,K
for w being Element of Union G,RK ex a being Element of G st w in Class RK,a
let K be closed Ideal of X; :: thesis: for RK being I-congruence of X,K
for w being Element of Union G,RK ex a being Element of G st w in Class RK,a
let RK be I-congruence of X,K; :: thesis: for w being Element of Union G,RK ex a being Element of G st w in Class RK,a
defpred S₁[ Element of Union G,RK, Element of Union G,RK, set ] means $3 = $1 \ $2;
set Z1 = union { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;
set Z2 = { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ;
let w be Element of Union G,RK; :: thesis: ex a being Element of G st w in Class RK,a
consider g being set such that
B1: ( w in g & g in { (Class RK,a) where a is Element of G : Class RK,a in the carrier of (X ./. RK) } ) by TARSKI:def 4;
consider a being Element of G such that
B3: ( g = Class RK,a & Class RK,a in the carrier of (X ./. RK) ) by B1;
take a ; :: thesis: w in Class RK,a
thus w in Class RK,a by B1, B3; :: thesis: verum