let X be set ; :: thesis: for U being Universe st X in U holds
( bool X in U & union X in U & meet X in U )
let U be Universe; :: thesis: ( X in U implies ( bool X in U & union X in U & meet X in U ) )
assume A1: X in U ; :: thesis: ( bool X in U & union X in U & meet X in U )
hence bool X in U by CLASSES1:def 2; :: thesis: ( union X in U & meet X in U )
U = Rank (On U) by Th50;
hence A2: union X in U by A1, CLASSES1:35; :: thesis: meet X in U
meet X c= union X by SETFAM_1:2;
hence meet X in U by A2, CLASSES1:def 1; :: thesis: verum