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

proof

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

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (ObjectDerivation C) . { the Object of C} or x in the carrier' of C )
assume x in (ObjectDerivation C) . { the Object of C} ; :: 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 Def2;
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in t holds
o is-connected-with x9 ) ) ;
hence x in the carrier' of C ; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) or x in the carrier of C )
assume x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) ; :: thesis: x in the carrier of C
then x in { o9 where o9 is Object of C : for a being Attribute of C st a in (ObjectDerivation C) . t holds
o9 is-connected-with a } by Def3;
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in (ObjectDerivation C) . t holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; :: thesis: verum

end;

then reconsider O = (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) as Subset of the carrier of C ;
set M9 = ConceptStr(# O,A #);
( the Object of C in { the Object of C} & t c= (AttributeDerivation C) . ((ObjectDerivation C) . t) ) by Th5, TARSKI:def 1;
then reconsider M9 = ConceptStr(# O,A #) as non empty ConceptStr over C by Def7;
(ObjectDerivation C) . the Extent of M9 = (ObjectDerivation C) . t by Th7
.= the Intent of M9 ;
then M9 is concept-like ;
hence ex b₁ being ConceptStr over C st
( b₁ is concept-like & not b₁ is empty ) ; :: thesis: verum