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