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 )

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

proof

assume A2:
for x being Element of IT holds x in U_FT x
; :: thesis: IT is filled
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;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

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