let R be RelStr ; :: thesis: for X being Subset of R

for x being set st X is lower & x in X holds

the InternalRel of R -Seg x c= X

let X be Subset of R; :: thesis: for x being set st X is lower & x in X holds

the InternalRel of R -Seg x c= X

let x be set ; :: thesis: ( X is lower & x in X implies the InternalRel of R -Seg x c= X )

assume A1: ( X is lower & x in X ) ; :: thesis: the InternalRel of R -Seg x c= X

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the InternalRel of R -Seg x or z in X )

assume z in the InternalRel of R -Seg x ; :: thesis: z in X

then [z,x] in the InternalRel of R by WELLORD1:1;

hence z in X by A1; :: thesis: verum

for x being set st X is lower & x in X holds

the InternalRel of R -Seg x c= X

let X be Subset of R; :: thesis: for x being set st X is lower & x in X holds

the InternalRel of R -Seg x c= X

let x be set ; :: thesis: ( X is lower & x in X implies the InternalRel of R -Seg x c= X )

assume A1: ( X is lower & x in X ) ; :: thesis: the InternalRel of R -Seg x c= X

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the InternalRel of R -Seg x or z in X )

assume z in the InternalRel of R -Seg x ; :: thesis: z in X

then [z,x] in the InternalRel of R by WELLORD1:1;

hence z in X by A1; :: thesis: verum