let C be initialized ConstructorSignature; :: thesis: for e being expression of C holds
( e is ground iff variables_in e = {} )
let e be expression of C; :: thesis: ( e is ground iff variables_in e = {} )
thus ( e is ground implies variables_in e = {} ) :: thesis: ( variables_in e = {} implies e is ground )

proof

assume Union (C variables_in e) = {} ; :: according to ABCMIZ_1:def 26 :: thesis: variables_in e = {}
hence variables_in e = {} by Th1, XBOOLE_1:3; :: thesis: verum

end;

assume that
A1: variables_in e = {} and
A2: Union (C variables_in e) <> {} ; :: according to ABCMIZ_1:def 26 :: thesis: contradiction
consider x being Element of Union (C variables_in e);
A3: ex y being set st
( y in dom (C variables_in e) & x in (C variables_in e) . y ) by A2, CARD_5:10;
A4: dom (C variables_in e) = the carrier of C by PARTFUN1:def 4
.= {a_Type,an_Adj,a_Term} by Def9 ;
A5: C variables_in e c= MSVars C by MSAFREE3:28;
A6: (MSVars C) . an_Adj = {} by Def25;
A7: (MSVars C) . a_Type = {} by Def25;
A8: (C variables_in e) . (an_Adj C) c= {} by A5, A6, PBOOLE:def 5;
(C variables_in e) . (a_Type C) c= {} by A5, A7, PBOOLE:def 5;
hence contradiction by A1, A3, A4, A8, ENUMSET1:def 1; :: thesis: verum