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