set X = the non empty finite set ;
reconsider T = {} as Relation of [: the non empty finite set ,F:], the non empty finite set by RELSET_1:12;
take TS = transition-system(# the non empty finite set ,T #); :: thesis: ( TS is strict & not TS is empty & TS is finite & TS is deterministic )
thus TS is strict ; :: thesis: ( not TS is empty & TS is finite & TS is deterministic )
thus not TS is empty ; :: thesis: ( TS is finite & TS is deterministic )
thus the carrier of TS is finite ; :: according to STRUCT_0:def 11 :: thesis: TS is deterministic
thus TS is deterministic ; :: thesis: verum