take c ; :: thesis: ex c being Element of SCM+FSA-Data-Loc st
( <*c*> = x `3_3 & c = c )
take c ; :: thesis: ( <*c*> = x `3_3 & c = c )
thus ( <*c*> = x `3_3 & c = c ) by A1, RECDEF_2:def 3; :: thesis: verum