let X be BCI-algebra; :: thesis: ConSet X = (LConSet X) /\ (RConSet X)
thus ConSet X c= (LConSet X) /\ (RConSet X) :: according to XBOOLE_0:def 10 :: thesis: (LConSet X) /\ (RConSet X) c= ConSet X

proof

( ConSet X c= LConSet X & ConSet X c= RConSet X ) by Th45, Th46;
hence ConSet X c= (LConSet X) /\ (RConSet X) by XBOOLE_1:19; :: thesis: verum

end;

thus (LConSet X) /\ (RConSet X) c= ConSet X :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (LConSet X) /\ (RConSet X) or x in ConSet X )
assume x in (LConSet X) /\ (RConSet X) ; :: thesis: x in ConSet X
then A1: ( x in LConSet X & x in RConSet X ) by XBOOLE_0:def 4;
then consider R being R-congruence of X such that
A2: x = R ;
consider L being L-congruence of X such that
A3: x = L by A1;
x is Congruence of X by A2, A3, Th36;
hence x in ConSet X ; :: thesis: verum

end;