set S = the non empty set ;
set o = the non-empty non empty PFuncFinSequence of the non empty set ;
set r = the Relation of the non empty set ;
take X = TRSStr(# the non empty set , the non-empty non empty PFuncFinSequence of the non empty set , the Relation of the non empty set #); :: thesis: ( not X is empty & X is non-empty & X is strict )
thus not the carrier of X is empty ; :: according to STRUCT_0:def 1 :: thesis: ( X is non-empty & X is strict )
thus the charact of X <> {} ; :: according to UNIALG_1:def 3 :: thesis: ( the charact of X is non-empty & X is strict )
thus ( the charact of X is non-empty & X is strict ) ; :: thesis: verum