let R be non empty transitive RelStr ; :: thesis: for X being Subset of R holds LAp X c= LAp (LAp X)
let X be Subset of R; :: thesis: LAp X c= LAp (LAp X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in LAp X or x in LAp (LAp X) )
assume x in LAp X ; :: thesis: x in LAp (LAp X)
then x in { u where u is Element of R : Class ( the InternalRel of R,u) c= X } by ROUGHS_1:def 4;
then consider y being Element of R such that
A1: ( y = x & Class ( the InternalRel of R,y) c= X ) ;
Class ( the InternalRel of R,y) c= LAp X
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Class ( the InternalRel of R,y) or t in LAp X )
assume t in Class ( the InternalRel of R,y) ; :: thesis: t in LAp X
then B0: [y,t] in the InternalRel of R by RELAT_1:169;
then b1: t in rng the InternalRel of R by XTUPLE_0:def 13;
Class ( the InternalRel of R,t) c= X
proof
let s be object ; :: according to TARSKI:def 3 :: thesis: ( not s in Class ( the InternalRel of R,t) or s in X )
assume s in Class ( the InternalRel of R,t) ; :: thesis: s in X
then B2: [t,s] in the InternalRel of R by RELAT_1:169;
then s in rng the InternalRel of R by XTUPLE_0:def 13;
then [y,s] in the InternalRel of R by B0, B2, b1, RELAT_2:def 8, ORDERS_2:def 3;
then s in Im ( the InternalRel of R,y) by RELAT_1:169;
hence s in X by A1; :: thesis: verum
end;
then t in { u where u is Element of R : Class ( the InternalRel of R,u) c= X } by b1;
hence t in LAp X by ROUGHS_1:def 4; :: thesis: verum
end;
then y in { u where u is Element of R : Class ( the InternalRel of R,u) c= LAp X } ;
hence x in LAp (LAp X) by ROUGHS_1:def 4, A1; :: thesis: verum