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