let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st A c= B holds
A ^i c= B ^i
let A, B be Subset of FT; :: thesis: ( A c= B implies A ^i c= B ^i )
assume A1: A c= B ; :: thesis: A ^i c= B ^i
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^i or x in B ^i )
assume A2: x in A ^i ; :: thesis: x in B ^i
then reconsider y = x as Element of FT ;
A3: U_FT y c= A by A2, FIN_TOPO:7;
for t being Element of FT st t in U_FT y holds
t in B by A3, A1;
then U_FT y c= B ;
hence x in B ^i ; :: thesis: verum