let U be Universe; :: thesis: for C being CategorySet holds
( C is U -set iff SetToCat C is U -element )
let C be CategorySet; :: thesis: ( C is U -set iff SetToCat C is U -element )
A1: C = [(C `1),(C `2),(C `3),(C `4),(C `5)] ;

hereby :: thesis: ( SetToCat C is U -element implies C is U -set )

assume C is U -set ; :: thesis: SetToCat C is U -element
then A2: ( C `1 is Element of U & C `2 is Element of U & C `3 is Element of U & C `4 is Element of U & C `5 is Element of U ) by A1, Th14;
ex y1, y2 being set ex y3, y4 being Function of y2,y1 ex y5 being PartFunc of [:y2,y2:],y2 st
( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & CatStr(# y1,y2,y3,y4,y5 #) is Category ) by Def27;
hence SetToCat C is U -element by A2, Def31; :: thesis: verum

end;

assume A3: SetToCat C is U -element ; :: thesis: C is U -set
set C2 = SetToCat C;
consider y1, y2 being set , y3, y4 being Function of y2,y1, y5 being PartFunc of [:y2,y2:],y2 such that
A4: ( y1 = C `1 & y2 = C `2 & y3 = C `3 & y4 = C `4 & y5 = C `5 & SetToCat C = CatStr(# y1,y2,y3,y4,y5 #) ) by Def31;
reconsider y1 = y1, y2 = y2 as Element of U by A4, A3;
reconsider y22 = [:y2,y2:] as Element of U ;
( y3 c= [:y2,y1:] & y4 c= [:y2,y1:] & y5 c= [:y22,y2:] ) ;
then reconsider y3 = y3, y4 = y4, y5 = y5 as Element of U by CLASSES4:13;
CatToSet (SetToCat C) = [y1,y2,y3,y4,y5] by A4;
then CatToSet (SetToCat C) is U -set ;
hence C is U -set by Th86; :: thesis: verum