let x be set ; :: according to CLASSES1:def 1 :: thesis: for b₁ being set holds
( not x in Sub_of_Fin X or not b₁ c= x or b₁ in Sub_of_Fin X )
let y be set ; :: thesis: ( not x in Sub_of_Fin X or not y c= x or y in Sub_of_Fin X )
assume ( x in Sub_of_Fin X & y c= x ) ; :: thesis: y in Sub_of_Fin X
hence y in Sub_of_Fin X by CLASSES1:def 1; :: thesis: verum