let n, m be Nat; :: thesis: ( n <= m implies InclPoset n is full SubRelStr of InclPoset m )

A1: the InternalRel of (InclPoset m) = RelIncl m by YELLOW_1:1;

assume n <= m ; :: thesis: InclPoset n is full SubRelStr of InclPoset m

then A2: Segm n c= Segm m by NAT_1:39;

A3: RelIncl n c= RelIncl m

then A4: the carrier of (InclPoset n) c= the carrier of (InclPoset m) by A2, YELLOW_1:1;

A5: the InternalRel of (InclPoset n) = RelIncl n by YELLOW_1:1;

then (RelIncl m) |_2 n = the InternalRel of (InclPoset n) by A2, WELLORD2:7;

then the InternalRel of (InclPoset n) = the InternalRel of (InclPoset m) |_2 the carrier of (InclPoset n) by A1, YELLOW_1:1;

hence InclPoset n is full SubRelStr of InclPoset m by A4, A5, A1, A3, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum

A1: the InternalRel of (InclPoset m) = RelIncl m by YELLOW_1:1;

assume n <= m ; :: thesis: InclPoset n is full SubRelStr of InclPoset m

then A2: Segm n c= Segm m by NAT_1:39;

A3: RelIncl n c= RelIncl m

proof

the carrier of (InclPoset m) = m
by YELLOW_1:1;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in RelIncl n or x in RelIncl m )

assume x in RelIncl n ; :: thesis: x in RelIncl m

then x in (RelIncl m) |_2 n by A2, WELLORD2:7;

hence x in RelIncl m by XBOOLE_0:def 4; :: thesis: verum

end;assume x in RelIncl n ; :: thesis: x in RelIncl m

then x in (RelIncl m) |_2 n by A2, WELLORD2:7;

hence x in RelIncl m by XBOOLE_0:def 4; :: thesis: verum

then A4: the carrier of (InclPoset n) c= the carrier of (InclPoset m) by A2, YELLOW_1:1;

A5: the InternalRel of (InclPoset n) = RelIncl n by YELLOW_1:1;

then (RelIncl m) |_2 n = the InternalRel of (InclPoset n) by A2, WELLORD2:7;

then the InternalRel of (InclPoset n) = the InternalRel of (InclPoset m) |_2 the carrier of (InclPoset n) by A1, YELLOW_1:1;

hence InclPoset n is full SubRelStr of InclPoset m by A4, A5, A1, A3, YELLOW_0:def 13, YELLOW_0:def 14; :: thesis: verum