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
A1: w in g and
A2: 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
A3: g = Class RK,a and
Class RK,a in the carrier of (X ./. RK) by A2;
take a ; :: thesis: w in Class RK,a
thus w in Class RK,a by A1, A3; :: thesis: verum