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 = {} ) by Th1, XBOOLE_1:3; :: thesis: ( variables_in e = {} implies e is ground )
assume that
A1: variables_in e = {} and
A2: Union (C variables_in e) <> {} ; :: according to ABCMIZ_1:def 26 :: thesis: contradiction
set x = the Element of Union (C variables_in e);
A3: ex y being object st
( y in dom (C variables_in e) & the Element of Union (C variables_in e) in (C variables_in e) . y ) by A2, CARD_5:2;
A4: dom (C variables_in e) = the carrier of C by PARTFUN1:def 2
.= {a_Type,an_Adj,a_Term} by Def9 ;
A5: C variables_in e c= MSVars C by MSAFREE3:27;
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;
(C variables_in e) . (a_Type C) c= {} by A5, A7;
hence contradiction by A1, A3, A4, A8, ENUMSET1:def 1; :: thesis: verum