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

{ 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

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
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;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