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

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