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
proof
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;
the carrier of (InclPoset m) = m by YELLOW_1:1;
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