consider o being Object of C;
set O = (AttributeDerivation C) . ((ObjectDerivation C) . {o});
set A = (ObjectDerivation C) . {o};
{o} c= the carrier of C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {o} or x in the carrier of C )
assume x in {o} ; :: thesis: x in the carrier of C
then x = o by TARSKI:def 1;
hence x in the carrier of C ; :: thesis: verum

end;

then reconsider t = {o} as Subset of the carrier of C ;
(AttributeDerivation C) . ((ObjectDerivation C) . {o}) c= the carrier of C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (AttributeDerivation C) . ((ObjectDerivation C) . {o}) or x in the carrier of C )
assume x in (AttributeDerivation C) . ((ObjectDerivation C) . {o}) ; :: thesis: x in the carrier of C
then x in { o' where o' is Object of C : for a being Attribute of C st a in (ObjectDerivation C) . t holds
o' is-connected-with a } by Def7;
then consider x' being Object of C such that
A1: ( x' = x & ( for a being Attribute of C st a in (ObjectDerivation C) . t holds
x' is-connected-with a ) ) ;
thus x in the carrier of C by A1; :: thesis: verum

end;

then reconsider O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) as Subset of the carrier of C ;
(ObjectDerivation C) . {o} c= the carrier' of C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (ObjectDerivation C) . {o} or x in the carrier' of C )
assume x in (ObjectDerivation C) . {o} ; :: thesis: x in the carrier' of C
then x in { a where a is Attribute of C : for o being Object of C st o in t holds
o is-connected-with a } by Def6;
then consider x' being Attribute of C such that
A2: ( x' = x & ( for o being Object of C st o in t holds
o is-connected-with x' ) ) ;
thus x in the carrier' of C by A2; :: thesis: verum

end;

then reconsider A = (ObjectDerivation C) . {o} as Subset of the carrier' of C ;
set M' = ConceptStr(# O,A #);
not ConceptStr(# O,A #) is empty

proof

A3: o in {o} by TARSKI:def 1;
t c= (AttributeDerivation C) . ((ObjectDerivation C) . t) by Th5;
hence not ConceptStr(# O,A #) is empty by A3, Def11; :: thesis: verum

end;

then reconsider M' = ConceptStr(# O,A #) as non empty ConceptStr of C ;
(ObjectDerivation C) . the Extent of M' = (ObjectDerivation C) . t by Th7
.= the Intent of M' ;
then M' is concept-like by Def13;
hence ex b₁ being ConceptStr of C st
( b₁ is concept-like & not b₁ is empty ) ; :: thesis: verum