thus ( IT is filled implies for x being Element of IT holds x in U_FT x ) :: thesis: ( ( for x being Element of IT holds x in U_FT x ) implies IT is filled )

proof

assume A1: IT is filled ; :: thesis: for x being Element of IT holds x in U_FT x
let x be Element of IT; :: thesis: x in U_FT x
x <= x by A1, ORDERS_2:1;
then [x,x] in the InternalRel of IT ;
hence x in U_FT x by EQREL_1:18; :: thesis: verum

end;

assume A2: for x being Element of IT holds x in U_FT x ; :: thesis: IT is filled
let x be object ; :: according to RELAT_2:def 1,ORDERS_2:def 2 :: thesis: ( not x in the carrier of IT or [x,x] in the InternalRel of IT )
assume x in the carrier of IT ; :: thesis: [x,x] in the InternalRel of IT
then reconsider x = x as Element of IT ;
x in U_FT x by A2;
hence [x,x] in the InternalRel of IT by EQREL_1:18; :: thesis: verum