let X be BCI-algebra; :: thesis: for A being Ideal of X
for a being Element of A holds initial_section a c= A
let A be Ideal of X; :: thesis: for a being Element of A holds initial_section a c= A
let a be Element of A; :: thesis: initial_section a c= A
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in initial_section a or b in A )
assume b in initial_section a ; :: thesis: b in A
then ex x1 being Element of X st
( b = x1 & x1 <= a ) ;
hence b in A by Th5; :: thesis: verum