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

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