let FT be non empty RelStr ; :: thesis: for A, B being Subset of st A c= B holds
A ^i c= B ^i
let A, B be Subset of ; :: thesis: ( A c= B implies A ^i c= B ^i )
assume A1: A c= B ; :: thesis: A ^i c= B ^i
let x be set ; :: 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 ;
A3: U_FT y c= A by A2, FIN_TOPO:12;
for t being Element of st t in U_FT y holds
t in B

proof

let t be Element of ; :: thesis: ( t in U_FT y implies t in B )
assume t in U_FT y ; :: thesis: t in B
then t in A by A3;
hence t in B by A1; :: thesis: verum

end;

then U_FT y c= B by SUBSET_1:7;
hence x in B ^i ; :: thesis: verum