let ti be INT-Expression of A,f; :: thesis: ( ti = leq (t1,t2) iff for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),0,1) )

A9: dom t1 = Funcs (X,INT) by FUNCT_2:def 1;

A10: dom t2 = Funcs (X,INT) by FUNCT_2:def 1;

A11: dom (leq (t1,t2)) = (dom t1) /\ (dom t2) by Def5;

hence ( ti = leq (t1,t2) implies for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),0,1) ) by A9, A10, Def5; :: thesis: ( ( for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),0,1) ) implies ti = leq (t1,t2) )

A12: dom ti = Funcs (X,INT) by FUNCT_2:def 1;

assume for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),0,1) ; :: thesis: ti = leq (t1,t2)

then for s being object st s in Funcs (X,INT) holds

ti . s = IFGT ((t1 . s),(t2 . s),0,1) ;

hence ti = leq (t1,t2) by A11, A9, A10, A12, Def5; :: thesis: verum

A9: dom t1 = Funcs (X,INT) by FUNCT_2:def 1;

A10: dom t2 = Funcs (X,INT) by FUNCT_2:def 1;

A11: dom (leq (t1,t2)) = (dom t1) /\ (dom t2) by Def5;

hence ( ti = leq (t1,t2) implies for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),0,1) ) by A9, A10, Def5; :: thesis: ( ( for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),0,1) ) implies ti = leq (t1,t2) )

A12: dom ti = Funcs (X,INT) by FUNCT_2:def 1;

assume for s being Element of Funcs (X,INT) holds ti . s = IFGT ((t1 . s),(t2 . s),0,1) ; :: thesis: ti = leq (t1,t2)

then for s being object st s in Funcs (X,INT) holds

ti . s = IFGT ((t1 . s),(t2 . s),0,1) ;

hence ti = leq (t1,t2) by A11, A9, A10, A12, Def5; :: thesis: verum