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

hence x in LAp (LAp X) by ROUGHS_1:def 4, A1; :: thesis: verum

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

then
y in { u where u is Element of R : Class ( the InternalRel of R,u) c= LAp X }
;
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

hence t in LAp X by ROUGHS_1:def 4; :: thesis: verum

end;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

then
t in { u where u is Element of R : Class ( the InternalRel of R,u) c= X }
by b1;
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;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

hence t in LAp X by ROUGHS_1:def 4; :: thesis: verum

hence x in LAp (LAp X) by ROUGHS_1:def 4, A1; :: thesis: verum