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 set ; :: 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 consider x1 being Element of X such that
A3: ( b = x1 & x1 <= a ) ;
thus b in A by A3, P141; :: thesis: verum