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 that
A1: o in A and
A2: A in X ; :: thesis: o is Element of V
A c= V by A2, ORDINAL1:def 2;
hence o is Element of V by A1; :: thesis: verum