[:{0},{0}:] c= [:{0},{0}:]
;

then reconsider R = [:{0},{0}:] as Relation of {0} ;

RelStr(# {0},R #) in fin_RelStr_sp

then reconsider R = [:{0},{0}:] as Relation of {0} ;

RelStr(# {0},R #) in fin_RelStr_sp

proof

hence
not fin_RelStr_sp is empty
; :: thesis: verum
set X = RelStr(# {0},R #);

A1: the carrier of RelStr(# {0},R #) in FinSETS by CLASSES2:56, CLASSES2:57;

thus RelStr(# {0},R #) in fin_RelStr_sp by A1, Def5; :: thesis: verum

end;A1: the carrier of RelStr(# {0},R #) in FinSETS by CLASSES2:56, CLASSES2:57;

thus RelStr(# {0},R #) in fin_RelStr_sp by A1, Def5; :: thesis: verum