let V be Universe; :: thesis: for X being Subclass of V
for o, A being set holds
( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) )
let X be Subclass of V; :: thesis: for o, A being set holds
( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) )
let o, A be set ; :: thesis: ( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) )
thus ( X c= V & ( o in X implies o is Element of V ) ) ; :: thesis: ( o in A & A in X implies o is Element of V )
assume A1: ( o in A & A in X ) ; :: thesis: o is Element of V
then A c= V by ORDINAL1:def 2;
hence o is Element of V by A1; :: thesis: verum