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

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