set S = { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ;
{ A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } c= Fin the carrier of C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } or x in Fin the carrier of C )
assume x in { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } ; :: thesis: x in Fin the carrier of C
then ex a being Element of Fin the carrier of C st
( x = a & the InternalRel of C linearly_orders a ) ;
hence x in Fin the carrier of C ; :: thesis: verum

end;

hence { A where A is Element of Fin the carrier of C : the InternalRel of C linearly_orders A } is Subset of (Fin the carrier of C) ; :: thesis: verum