let L be RelStr ; :: thesis: for S being full SubRelStr of L
for R being SubRelStr of S holds
( R is full iff R is full SubRelStr of L )
let S be full SubRelStr of L; :: thesis: for R being SubRelStr of S holds
( R is full iff R is full SubRelStr of L )
let R be SubRelStr of S; :: thesis: ( R is full iff R is full SubRelStr of L )
reconsider R9 = R as SubRelStr of L by YELLOW_6:7;
A1: the carrier of R c= the carrier of S by YELLOW_0:def 13;
hereby :: thesis: ( R is full SubRelStr of L implies R is full )
assume R is full ; :: thesis: R is full SubRelStr of L
then the InternalRel of R = the InternalRel of S |_2 the carrier of R
.= ( the InternalRel of L |_2 the carrier of S) |_2 the carrier of R by YELLOW_0:def 14
.= the InternalRel of L |_2 the carrier of R9 by A1, WELLORD1:22 ;
hence R is full SubRelStr of L by YELLOW_0:def 14; :: thesis: verum
end;
assume A2: R is full SubRelStr of L ; :: thesis: R is full
( the InternalRel of L |_2 the carrier of S) |_2 the carrier of R = the InternalRel of L |_2 the carrier of R by A1, WELLORD1:22
.= the InternalRel of R by A2, YELLOW_0:def 14 ;
hence the InternalRel of R = the InternalRel of S |_2 the carrier of R by YELLOW_0:def 14; :: according to YELLOW_0:def 14 :: thesis: verum