let X be BCI-algebra; :: thesis: ConSet X = (LConSet X) /\ (RConSet X)
( 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; :: according to XBOOLE_0:def 10 :: thesis: (LConSet X) /\ (RConSet X) c= ConSet X
thus (LConSet X) /\ (RConSet X) c= ConSet X :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (LConSet X) /\ (RConSet X) or x in ConSet X )
assume A1: x in (LConSet X) /\ (RConSet X) ; :: thesis: x in ConSet X
then x in RConSet X by XBOOLE_0:def 4;
then A2: ex R being R-congruence of X st x = R ;
x in LConSet X by A1, XBOOLE_0:def 4;
then ex L being L-congruence of X st x = L ;
then x is Congruence of X by A2, Th36;
hence x in ConSet X ; :: thesis: verum
end;